:: deftheorem defines (Co) GTARSKI3:def 25 :
for S being TarskiGeometryStruct holds
( S is (Co) iff for X, Y being set st ex a being POINT of S st
for x, y being POINT of S st x in X & y in Y holds
between a,x,y holds
ex b being POINT of S st
for x, y being POINT of S st x in X & y in Y holds
between x,b,y );