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 A1: ( a in C & b in C & c in C & 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 ) by Def1; :: thesis: verum

end;

suppose A2: ( 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 A3: LE d,c,C by A1, JORDAN16:11;
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, JORDAN16:11;

suppose A4: 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 A1, JORDAN16:11;
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 A2, A3, A4, Def1; :: 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 A2, Def1; :: thesis: verum

end;

end;

end;

end;

suppose A5: ( 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 A6: LE c,b,C by A1, JORDAN16:11;
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 A1, JORDAN16:11;

suppose A7: 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, JORDAN16:11;
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, Def1; :: thesis: verum

end;

suppose A8: 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, JORDAN16:11;

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 A5, A8, Def1; :: thesis: verum

end;

suppose A9: 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, JORDAN16:11;
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, A8, A9, Def1; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

suppose A10: ( 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 A11: ( LE c,b,C & LE d,c,C ) by A1, JORDAN16:11;
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, JORDAN16:11;

suppose A12: 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, JORDAN16:11;
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 A11, A12, Def1; :: 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 A10, A11, Def1; :: thesis: verum

end;

end;

end;

end;

suppose A13: ( 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 A14: LE b,a,C by A1, JORDAN16:11;
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, JORDAN16:11;

suppose A15: 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, JORDAN16:11;
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, A15, Def1; :: 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 A13, Def1; :: thesis: verum

end;

end;

end;

end;

suppose A16: ( 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 A17: ( LE b,a,C & LE d,c,C ) by A1, JORDAN16:11;
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, JORDAN16:11;

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 A17, Def1; :: thesis: verum

end;

suppose A18: 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 a,c,C or LE c,a,C ) & ( LE b,d,C or LE d,b,C ) ) by A1, JORDAN16:11;
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 A16, A17, A18, Def1; :: thesis: verum

end;

end;

end;

end;

suppose A19: ( 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 A20: ( LE b,a,C & LE c,b,C ) by A1, JORDAN16:11;
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, JORDAN16:11;

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 A20, Def1; :: thesis: verum

end;

suppose A21: 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 A1, JORDAN16:11;
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 A19, A20, A21, Def1; :: thesis: verum

end;

end;

end;

end;

suppose ( 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 ( LE b,a,C & LE c,b,C & LE d,c,C ) by A1, JORDAN16:11;
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 Def1; :: thesis: verum

end;

end;