let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c, d being POINT of S holds
( a,b <= c,d iff ex x being POINT of S st
( between a,b,x & a,x equiv c,d ) )
let a, b, c, d be POINT of S; :: thesis: ( a,b <= c,d iff ex x being POINT of S st
( between a,b,x & a,x equiv c,d ) )
A1: ( a,b <= c,d implies ex x being POINT of S st
( between a,b,x & a,x equiv c,d ) )
proof
assume a,b <= c,d ; :: thesis: ex x being POINT of S st
( between a,b,x & a,x equiv c,d )
then consider y being POINT of S such that
A2: ( between c,y,d & a,b equiv c,y ) ;
Collinear c,y,d by A2;
then consider x being POINT of S such that
A3: c,y,d cong a,b,x by A2, Satz2p2, Satz4p14;
a,x equiv c,d by A3, Satz2p2;
hence ex x being POINT of S st
( between a,b,x & a,x equiv c,d ) by A2, A3, Satz4p6; :: thesis: verum
end;
( ex x being POINT of S st
( between a,b,x & a,x equiv c,d ) implies a,b <= c,d )
proof
assume ex x being POINT of S st
( between a,b,x & a,x equiv c,d ) ; :: thesis: a,b <= c,d
then consider x being POINT of S such that
A4: ( between a,b,x & a,x equiv c,d ) ;
A5: Collinear x,a,b by A4;
x,a equiv c,d by A4, Satz2p4;
then consider y being POINT of S such that
A6: x,a,b cong d,c,y by A5, Satz2p5, Satz4p14;
a,b,x cong c,y,d
proof
A9: a,x equiv c,d
proof
a,x equiv d,c by A6, Satz2p4;
hence a,x equiv c,d by Satz2p5; :: thesis: verum
end;
b,x equiv y,d
proof
b,x equiv d,y by A6, Satz2p4;
hence b,x equiv y,d by Satz2p5; :: thesis: verum
end;
hence a,b,x cong c,y,d by A6, A9; :: thesis: verum
end;
hence a,b <= c,d by A4, Satz4p6; :: thesis: verum
end;
hence ( a,b <= c,d iff ex x being POINT of S st
( between a,b,x & a,x equiv c,d ) ) by A1; :: thesis: verum