for S being satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_Lower_Dimension_Axiom TarskiGeometryStruct ex a, b, c being POINT of S st
( not between a,b,c & not between b,c,a & not between c,a,b & a <> b & b <> c & c <> a )