Do Tarski's (geometry) axioms imply that all zero segments are congruent? Tarski's axioms are an alternate formalization of geometry (similar to axiom sets of Euclid and later Hilbert). Do these axioms imply:
$$\forall\; x,y\in \text{points},\; x x\equiv y y?$$
If yes, what  is the proof? My feeling is that the proof must use Tarski's Identity of Congruence
    $$xy\equiv zz \rightarrow x = y,$$
but I am unable to find a proof.

Let $y$ and $v$ be arbitrary. Let $z=u=y$ and $w=v$. By the segment construction axiom, there exists $x$ such that $Bvyx$ and $yx=vy$. Then, the hypothesis of the axiom of Euclid (form A using the same letters as I have used here) is satisfied, so we conclude $yz\equiv vw$. But indeed $y=z$ and $v=w$ so we have $yy\equiv vv$. Since $y$ and $v$ were arbitrary, we conclude $\forall y\forall v (yy\equiv vv)$.
I implicitly used a couple facts without stating which you should try to prove. Namely, $Byyy$ is a tautology, and $Bvyx$ iff $Bxyv$.
