:: deftheorem defines satisfying_A11 GTARSKI2:def 10 :
for S being TarskiGeometryStruct holds
( S is satisfying_A11 iff for X, Y being Subset of S 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 );