:: deftheorem defines (RE) GTARSKI3:def 15 :
for S being TarskiGeometryStruct holds
( S is (RE) iff for a, b being POINT of S holds a,b equiv b,a );