:: deftheorem defines equiv GTARSKI1:def 2 :
for S being TarskiGeometryStruct
for a, b, c, d being POINT of S holds
( a,b equiv c,d iff [[a,b],[c,d]] in the Equidistance of S );