:: deftheorem defines satisfying_A9 GTARSKI2:def 8 :
for S being TarskiGeometryStruct holds
( S is satisfying_A9 iff for a, b, c, p, q being POINT of S st p <> q & a,p equiv a,q & b,p equiv b,q & c,p equiv c,q & not between a,b,c & not between b,c,a holds
between c,a,b );