let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, x, y being POINT of S st a <> b & x <> y & Line (a,b) = Line (x,y) holds
a,b equal_line x,y
let a, b, x, y be POINT of S; :: thesis: ( a <> b & x <> y & Line (a,b) = Line (x,y) implies a,b equal_line x,y )
assume that
A1: a <> b and
A1A: x <> y and
A2: Line (a,b) = Line (x,y) ; :: thesis: a,b equal_line x,y
for c being POINT of S holds
( c on_line a,b iff c on_line x,y )
proof
let c be POINT of S; :: thesis: ( c on_line a,b iff c on_line x,y )
hereby :: thesis: ( c on_line x,y implies c on_line a,b )
assume c on_line a,b ; :: thesis: c on_line x,y
then Collinear a,b,c ;
then c in Line (x,y) by A2;
then ex z being POINT of S st
( c = z & Collinear x,y,z ) ;
hence c on_line x,y by A1A; :: thesis: verum
end;
assume c on_line x,y ; :: thesis: c on_line a,b
then Collinear x,y,c ;
then c in Line (a,b) by A2;
then ex z being POINT of S st
( c = z & Collinear a,b,z ) ;
hence c on_line a,b by A1; :: thesis: verum
end;
hence a,b equal_line x,y by A1, A1A; :: thesis: verum