theorem :: GTARSKI1:44

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