let S be 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
let a, b, y be POINT of S; ( 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 )
; 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; verum