let a, b, p, q, r, s be POINT of TarskiEuclid2Space; :: according to GTARSKI1:def 6 :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: verum