let C be Simple_closed_curve; :: thesis: for a, b, c, d being Point of (TOP-REAL 2) st a in C & b in C & c in C & d in C & not a,b,c,d are_in_this_order_on C & not a,b,d,c are_in_this_order_on C & not a,c,b,d are_in_this_order_on C & not a,c,d,b are_in_this_order_on C & not a,d,b,c are_in_this_order_on C holds
a,d,c,b are_in_this_order_on C
let a, b, c, d be Point of (TOP-REAL 2); :: thesis: ( a in C & b in C & c in C & d in C & not a,b,c,d are_in_this_order_on C & not a,b,d,c are_in_this_order_on C & not a,c,b,d are_in_this_order_on C & not a,c,d,b are_in_this_order_on C & not a,d,b,c are_in_this_order_on C implies a,d,c,b are_in_this_order_on C )
assume that
A1: a in C and
A2: b in C and
A3: c in C and
A4: d in C ; :: thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )

per cases ( ( LE a,b,C & LE b,c,C & LE c,d,C ) or ( LE a,b,C & LE b,c,C & not LE c,d,C ) or ( LE a,b,C & not LE b,c,C & LE c,d,C ) or ( LE a,b,C & not LE b,c,C & not LE c,d,C ) or ( not LE a,b,C & LE b,c,C & LE c,d,C ) or ( not LE a,b,C & LE b,c,C & not LE c,d,C ) or ( not LE a,b,C & not LE b,c,C & LE c,d,C ) or ( not LE a,b,C & not LE b,c,C & not LE c,d,C ) ) ;

suppose ( LE a,b,C & LE b,c,C & LE c,d,C ) ; :: thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )

hence ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) ; :: thesis: verum

end;

suppose A5: ( LE a,b,C & LE b,c,C & not LE c,d,C ) ; :: thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )

then A6: LE d,c,C by A3, A4, JORDAN16:7;
thus ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) :: thesis: verum

proof

per cases ( LE a,d,C or LE d,a,C ) by A1, A4, JORDAN16:7;

suppose A7: LE a,d,C ; :: thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )

( LE b,d,C or LE d,b,C ) by A2, A4, JORDAN16:7;
hence ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) by A5, A6, A7; :: thesis: verum

end;

suppose LE d,a,C ; :: thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )

hence ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) by A5; :: thesis: verum

end;

end;

end;

end;

suppose A8: ( LE a,b,C & not LE b,c,C & LE c,d,C ) ; :: thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )

then A9: LE c,b,C by A2, A3, JORDAN16:7;
thus ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) :: thesis: verum

proof

per cases ( LE b,d,C or LE d,b,C ) by A2, A4, JORDAN16:7;

suppose A10: LE b,d,C ; :: thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )

( LE a,c,C or LE c,a,C ) by A1, A3, JORDAN16:7;
hence ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) by A8, A9, A10; :: thesis: verum

end;

suppose A11: LE d,b,C ; :: thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )

thus ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) :: thesis: verum

proof

per cases ( LE a,c,C or LE c,a,C ) by A1, A3, JORDAN16:7;

suppose LE a,c,C ; :: thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )

hence ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) by A8, A11; :: thesis: verum

end;

suppose A12: LE c,a,C ; :: thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )

( LE a,d,C or LE d,a,C ) by A1, A4, JORDAN16:7;
hence ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) by A8, A11, A12; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

suppose A13: ( LE a,b,C & not LE b,c,C & not LE c,d,C ) ; :: thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )

then A14: LE d,c,C by A3, A4, JORDAN16:7;
A15: LE c,b,C by A2, A3, A13, JORDAN16:7;
thus ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) :: thesis: verum

proof

per cases ( LE a,c,C or LE c,a,C ) by A1, A3, JORDAN16:7;

suppose A16: LE a,c,C ; :: thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )

( LE a,d,C or LE d,a,C ) by A1, A4, JORDAN16:7;
hence ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) by A15, A14, A16; :: thesis: verum

end;

suppose LE c,a,C ; :: thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )

hence ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) by A13, A14; :: thesis: verum

end;

end;

end;

end;

suppose A17: ( not LE a,b,C & LE b,c,C & LE c,d,C ) ; :: thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )

then A18: LE b,a,C by A1, A2, JORDAN16:7;
thus ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) :: thesis: verum

proof

per cases ( LE a,d,C or LE d,a,C ) by A1, A4, JORDAN16:7;

suppose A19: LE a,d,C ; :: thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )

( LE a,c,C or LE c,a,C ) by A1, A3, JORDAN16:7;
hence ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) by A17, A18, A19; :: thesis: verum

end;

suppose LE d,a,C ; :: thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )

hence ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) by A17; :: thesis: verum

end;

end;

end;

end;

suppose A20: ( not LE a,b,C & LE b,c,C & not LE c,d,C ) ; :: thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )

then A21: ( LE b,a,C & LE d,c,C ) by A1, A2, A3, A4, JORDAN16:7;
thus ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) :: thesis: verum

proof

per cases ( LE a,d,C or LE d,a,C ) by A1, A4, JORDAN16:7;

suppose LE a,d,C ; :: thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )

hence ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) by A21; :: thesis: verum

end;

suppose A22: LE d,a,C ; :: thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )

A23: ( LE b,d,C or LE d,b,C ) by A2, A4, JORDAN16:7;
( LE a,c,C or LE c,a,C ) by A1, A3, JORDAN16:7;
hence ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) by A20, A21, A22, A23; :: thesis: verum

end;

end;

end;

end;

suppose A24: ( not LE a,b,C & not LE b,c,C & LE c,d,C ) ; :: thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )

then A25: ( LE b,a,C & LE c,b,C ) by A1, A2, A3, JORDAN16:7;
thus ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) :: thesis: verum

proof

per cases ( LE a,d,C or LE d,a,C ) by A1, A4, JORDAN16:7;

suppose LE a,d,C ; :: thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )

hence ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) by A25; :: thesis: verum

end;

suppose A26: LE d,a,C ; :: thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )

( LE b,d,C or LE d,b,C ) by A2, A4, JORDAN16:7;
hence ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) by A24, A25, A26; :: thesis: verum

end;

end;

end;

end;

suppose A27: ( not LE a,b,C & not LE b,c,C & not LE c,d,C ) ; :: thesis: ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C )

then A28: LE d,c,C by A3, A4, JORDAN16:7;
( LE b,a,C & LE c,b,C ) by A1, A2, A3, A27, JORDAN16:7;
hence ( a,b,c,d are_in_this_order_on C or a,b,d,c are_in_this_order_on C or a,c,b,d are_in_this_order_on C or a,c,d,b are_in_this_order_on C or a,d,b,c are_in_this_order_on C or a,d,c,b are_in_this_order_on C ) by A28; :: thesis: verum

end;

end;