:: deftheorem defines (TE) GTARSKI3:def 16 :
for S being TarskiGeometryStruct holds
( S is (TE) iff for a, b, p, q, r, s being POINT of S st a,b equiv p,q & a,b equiv r,s holds
p,q equiv r,s );