:: deftheorem defines (IE) GTARSKI3:def 17 :
for S being TarskiGeometryStruct holds
( S is (IE) iff for a, b, c being POINT of S st a,b equiv c,c holds
a = b );