theorem :: GTARSKI1:42

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, d being POINT of S st a <> b & c <> d & a,b equal_line c,d holds
c,d equal_line a,b ;