let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, x, y being POINT of S st a <> b & x <> y & a on_line x,y & b on_line x,y holds
x,y equal_line a,b
let a, b, x, y be POINT of S; :: thesis: ( a <> b & x <> y & a on_line x,y & b on_line x,y implies x,y equal_line a,b )
assume H1: ( a <> b & x <> y ) ; :: thesis: ( not a on_line x,y or not b on_line x,y or x,y equal_line a,b )
then P2: b,a equal_line a,b by LineEqA1;
assume H2: ( a on_line x,y & b on_line x,y ) ; :: thesis: x,y equal_line a,b

per cases ( x = b or x <> b ) ;

suppose x = b ; :: thesis: x,y equal_line a,b

then x,y equal_line b,a by H1, H2, I1part2;
hence x,y equal_line a,b by P2; :: thesis: verum

end;

suppose x <> b ; :: thesis: x,y equal_line a,b

then P4: x,y equal_line x,b by H2, I1part2;
then x,b equal_line a,b by H1, I1part2Reverse, H2;
hence x,y equal_line a,b by P4; :: thesis: verum

end;

end;