theorem :: GTARSKI1:43

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