:: deftheorem defines satisfying_BetweennessIdentity GTARSKI1:def 10 :
for S being TarskiGeometryStruct holds
( S is satisfying_BetweennessIdentity iff for a, b being POINT of S st between a,b,a holds
a = b );