:: deftheorem defines satisfying_A8 GTARSKI2:def 7 :
for S being TarskiGeometryStruct holds
( S is satisfying_A8 iff ex a, b, c being POINT of S st
( not between a,b,c & not between b,c,a & not between c,a,b ) );