let a, b, p, q, r, s be POINT of TarskiEuclid2Space; GTARSKI1:def 6 ( not a,b equiv p,q or not a,b equiv r,s or p,q equiv r,s )
assume
( a,b equiv p,q & a,b equiv r,s )
; p,q equiv r,s
then
( dist (a,b) = dist (p,q) & dist (a,b) = dist (r,s) )
by GTARSKI1:def 15;
hence
p,q equiv r,s
by GTARSKI1:def 15; verum