theorem I1part2Reverse: :: GTARSKI1:45

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