let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: 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
let a, b, y be POINT of S; :: thesis: ( a <> b & b <> y & y on_line a,b implies a,b equal_line y,b )
assume H1: ( a <> b & b <> y & y on_line a,b ) ; :: thesis: a,b equal_line y,b
then Y1: ( a,b equal_line b,a & b,y equal_line y,b ) by LineEqA1;
then b,a equal_line b,y by H1, I1part2;
then a,b equal_line b,y by Y1;
hence a,b equal_line y,b by Y1; :: thesis: verum