let P be Simple_closed_curve; :: thesis: for c, d, a, b being Point of (TOP-REAL 2) st c <> d & a,b,c,d are_in_this_order_on P holds
ex e being Point of (TOP-REAL 2) st
( e <> c & e <> d & b,c,e,d are_in_this_order_on P )
let c, d, a, b be Point of (TOP-REAL 2); :: thesis: ( c <> d & a,b,c,d are_in_this_order_on P implies ex e being Point of (TOP-REAL 2) st
( e <> c & e <> d & b,c,e,d are_in_this_order_on P ) )
assume that
A1: c <> d and
A2: ( ( 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: ex e being Point of (TOP-REAL 2) st
( e <> c & e <> d & b,c,e,d are_in_this_order_on P )

per cases ( ( 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 ) ) by A2;

suppose that A3: ( LE a,b,P & LE b,c,P ) and
A4: LE c,d,P ; :: thesis: ex e being Point of (TOP-REAL 2) st
( e <> c & e <> d & b,c,e,d are_in_this_order_on P )

consider e being Point of (TOP-REAL 2) such that
A5: ( e <> c & e <> d & LE c,e,P & LE e,d,P ) by A1, A4, Th8;
take e ; :: thesis: ( e <> c & e <> d & b,c,e,d are_in_this_order_on P )
thus ( e <> c & e <> d & b,c,e,d are_in_this_order_on P ) by A3, A5, Def1; :: thesis: verum

end;

suppose that A6: LE b,c,P and
A7: LE c,d,P and
LE d,a,P ; :: thesis: ex e being Point of (TOP-REAL 2) st
( e <> c & e <> d & b,c,e,d are_in_this_order_on P )

consider e being Point of (TOP-REAL 2) such that
A8: ( e <> c & e <> d & LE c,e,P & LE e,d,P ) by A1, A7, Th8;
take e ; :: thesis: ( e <> c & e <> d & b,c,e,d are_in_this_order_on P )
thus ( e <> c & e <> d & b,c,e,d are_in_this_order_on P ) by A6, A8, Def1; :: thesis: verum

end;

suppose that A9: LE c,d,P and
A10: LE d,a,P and
A11: LE a,b,P ; :: thesis: ex e being Point of (TOP-REAL 2) st
( e <> c & e <> d & b,c,e,d are_in_this_order_on P )

consider e being Point of (TOP-REAL 2) such that
A12: ( e <> c & e <> d & LE c,e,P & LE e,d,P ) by A1, A9, Th8;
take e ; :: thesis: ( e <> c & e <> d & b,c,e,d are_in_this_order_on P )
LE d,b,P by A10, A11, JORDAN6:73;
hence ( e <> c & e <> d & b,c,e,d are_in_this_order_on P ) by A12, Def1; :: thesis: verum

end;

suppose that A13: LE d,a,P and
A14: LE a,b,P and
A15: LE b,c,P ; :: thesis: ex e being Point of (TOP-REAL 2) st
( e <> c & e <> d & b,c,e,d are_in_this_order_on P )

thus ex e being Point of (TOP-REAL 2) st
( e <> c & e <> d & b,c,e,d are_in_this_order_on P ) :: thesis: verum

proof

A16: LE d,b,P by A13, A14, JORDAN6:73;

per cases ( d = W-min P or d <> W-min P ) ;

suppose A17: d = W-min P ; :: thesis: ex e being Point of (TOP-REAL 2) st
( e <> c & e <> d & b,c,e,d are_in_this_order_on P )

c in P by A15, JORDAN7:5;
then consider e being Point of (TOP-REAL 2) such that
A18: e <> c and
A19: LE c,e,P by Th7;
take e ; :: thesis: ( e <> c & e <> d & b,c,e,d are_in_this_order_on P )
thus e <> c by A18; :: thesis: ( e <> d & b,c,e,d are_in_this_order_on P )
thus e <> d by A1, A17, A19, JORDAN7:2; :: thesis: b,c,e,d are_in_this_order_on P
thus b,c,e,d are_in_this_order_on P by A15, A16, A19, Def1; :: thesis: verum

end;

suppose A20: d <> W-min P ; :: thesis: ex e being Point of (TOP-REAL 2) st
( e <> c & e <> d & b,c,e,d are_in_this_order_on P )

take e = W-min P; :: thesis: ( e <> c & e <> d & b,c,e,d are_in_this_order_on P )
d in P by A13, JORDAN7:5;
then A21: LE e,d,P by JORDAN7:3;

now

assume A22: e = c ; :: thesis: contradiction
LE d,c,P by A15, A16, JORDAN6:73;
hence contradiction by A1, A21, A22, JORDAN6:72; :: thesis: verum

end;

hence e <> c ; :: thesis: ( e <> d & b,c,e,d are_in_this_order_on P )
thus e <> d by A20; :: thesis: b,c,e,d are_in_this_order_on P
thus b,c,e,d are_in_this_order_on P by A15, A16, A21, Def1; :: thesis: verum

end;

end;

end;

end;

end;