for S being non empty satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, c9 being POINT of S st a <> b & c <> c9 & ( c in Line (a,b) or c in Line (b,a) ) & ( c9 in Line (a,b) or c9 in Line (b,a) ) holds
( Line (c,c9) = Line (a,b) & Line (c,c9) = Line (b,a) & Line (c9,c) = Line (b,a) & Line (c9,c) = Line (a,b) )