let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c, d being POINT of S holds
( a,b <= c,d or c,d <= a,b )
let a, b, c, d be POINT of S; :: thesis: ( a,b <= c,d or c,d <= a,b )
consider x being POINT of S such that
A1: ( between b,a,x & a,x equiv c,d ) by GTARSKI1:def 8;
consider y being POINT of S such that
A2: ( between x,a,y & a,y equiv c,d ) by GTARSKI1:def 8;
A3: ( not x = a or a,b <= c,d or c,d <= a,b )

proof

assume x = a ; :: thesis: ( a,b <= c,d or c,d <= a,b )
then A4: c = d by A1, Satz2p2, GTARSKI1:def 7;
ex q being POINT of S st
( between c,c,q & c,q equiv a,b ) by GTARSKI1:def 8;
hence ( a,b <= c,d or c,d <= a,b ) by A4, Satz5p5; :: thesis: verum

end;

( not x <> a or a,b <= c,d or c,d <= a,b )

proof

assume A5: x <> a ; :: thesis: ( a,b <= c,d or c,d <= a,b )
A6: between x,a,b by A1, Satz3p2;
then A7: ( between x,y,b or between x,b,y ) by A2, A5, Satz5p1;
( between x,y,b implies c,d <= a,b )

proof

assume between x,y,b ; :: thesis: c,d <= a,b
then between a,y,b by A2, Satz3p6p1;
hence c,d <= a,b by A2, Satz2p2; :: thesis: verum

end;

hence ( a,b <= c,d or c,d <= a,b ) by A2, A6, A7, Satz3p6p1, Satz5p5; :: thesis: verum

end;

hence ( a,b <= c,d or c,d <= a,b ) by A3; :: thesis: verum