theorem :: GTARSKI4:41

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, c, d, x, p, q being POINT of S st c in Line (a,b) & d in Line (a,b) & a <> b & c <> d holds
Line (a,b) = Line (c,d) by Prelim11;