let P be Simple_closed_curve; :: thesis: for a, b, c, d being Point of (TOP-REAL 2) st a,b,c,d are_in_this_order_on P holds
b,c,d,a are_in_this_order_on P
let a, b, c, d be Point of (TOP-REAL 2); :: thesis: ( a,b,c,d are_in_this_order_on P implies b,c,d,a are_in_this_order_on P )
assume ( ( LE a,b,P & LE b,c,P & LE c,d,P ) or ( LE b,c,P & LE c,d,P & LE d,a,P ) or ( LE c,d,P & LE d,a,P & LE a,b,P ) or ( LE d,a,P & LE a,b,P & LE b,c,P ) ) ; :: according to JORDAN17:def 1 :: thesis: b,c,d,a are_in_this_order_on P
hence ( ( LE b,c,P & LE c,d,P & LE d,a,P ) or ( LE c,d,P & LE d,a,P & LE a,b,P ) or ( LE d,a,P & LE a,b,P & LE b,c,P ) or ( LE a,b,P & LE b,c,P & LE c,d,P ) ) ; :: according to JORDAN17:def 1 :: thesis: verum