let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c, d being POINT of S st a,b <= c,d & c,d <= a,b holds
a,b equiv c,d
let a, b, c, d be POINT of S; :: thesis: ( a,b <= c,d & c,d <= a,b implies a,b equiv c,d )
assume A1: ( a,b <= c,d & c,d <= a,b ) ; :: thesis: a,b equiv c,d
then consider y being POINT of S such that
A2: ( between c,y,d & a,b equiv c,y ) ;
consider p being POINT of S such that
A3: ( between c,d,p & c,p equiv a,b ) by A1, Satz5p5;
consider q being POINT of S such that
A4: ( between a,q,b & c,d equiv a,q ) by A1;
consider r being POINT of S such that
A5: ( between d,c,r & c,r equiv a,b ) by GTARSKI1:def 8;
A6: ( c = y implies a,b equiv c,d )
proof
assume A7: c = y ; :: thesis: a,b equiv c,d
then a = b by A2, GTARSKI1:def 7;
then a = q by A4, GTARSKI1:def 10;
hence a,b equiv c,d by A7, A2, A4, GTARSKI1:def 7; :: thesis: verum
end;
( c <> y implies a,b equiv c,d )
proof
assume A8: c <> y ; :: thesis: a,b equiv c,d
A9: ( between d,y,c & between p,d,c ) by A2, A3, Satz3p2;
A10: r <> c
proof
assume r = c ; :: thesis: contradiction
then a = b by A5, Satz2p2, GTARSKI1:def 7;
hence contradiction by A2, Satz2p2, A8, GTARSKI1:def 7; :: thesis: verum
end;
A11: between r,c,y
proof
between y,c,r by A5, A9, Satz3p6p1;
hence between r,c,y by Satz3p2; :: thesis: verum
end;
A12: c <> d by A2, A8, GTARSKI1:def 10;
A13: between r,c,p
proof
between r,c,d by A5, Satz3p2;
hence between r,c,p by A3, A12, Satz3p7p2; :: thesis: verum
end;
c,y equiv a,b by A2, Satz2p2;
then y = p by A3, A10, A11, A13, Satz2p12;
then ( between d,p,c & between p,d,c ) by A2, A3, Satz3p2;
then p = d by Satz3p4;
hence a,b equiv c,d by A3, Satz2p2; :: thesis: verum
end;
hence a,b equiv c,d by A6; :: thesis: verum