let C be Simple_closed_curve; :: thesis: for a, b, c, d being Point of () 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 (); :: 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 )
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 ;
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 ;
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 ;
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;
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 ;
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 ;
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 ;
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 ;
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 ;
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 ;
A15: LE c,b,C by ;
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 ;
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 ;
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 ; :: 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 ;
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 ;
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 ;
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 ; :: 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 ;
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 ;
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 ;
( LE a,c,C or LE c,a,C ) by ;
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 ;
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 ;
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 ;
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 ; :: 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 ;
( LE b,a,C & LE c,b,C ) by ;
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;