:: deftheorem defines (RE') GTARSKI3:def 27 :
for S being TarskiGeometryStruct holds
( S is (RE') iff for a, b, c, d being POINT of S st a <> b & between b,a,c holds
d,c equiv c,d );