theorem I1part2: :: GTARSKI1:39

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, x being POINT of S st a <> b & a <> x & x on_line a,b holds
a,b equal_line a,x