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

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

end;

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

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

end;

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

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

proof

A10: LE d,b,P by A8, A9, JORDAN6:58;

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

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

b in P by A9, JORDAN7:5;
then consider e being Point of (TOP-REAL 2) such that
A12: e <> b and
A13: LE b,e,P by Th7;
take e ; :: thesis: ( e <> b & e <> c & b,e,c,d are_in_this_order_on P )
thus e <> b by A12; :: thesis: ( e <> c & b,e,c,d are_in_this_order_on P )
thus e <> c by A1, A11, A13, JORDAN7:2; :: thesis: b,e,c,d are_in_this_order_on P
thus b,e,c,d are_in_this_order_on P by A7, A10, A13; :: thesis: verum

end;

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

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

now :: thesis: not e = b

LE c,a,P by A7, A8, JORDAN6:58;
then A16: LE c,b,P by A9, JORDAN6:58;
assume e = b ; :: thesis: contradiction
hence contradiction by A1, A15, A16, JORDAN6:57; :: thesis: verum

end;

hence e <> b ; :: thesis: ( e <> c & b,e,c,d are_in_this_order_on P )
thus e <> c by A14; :: thesis: b,e,c,d are_in_this_order_on P
thus b,e,c,d are_in_this_order_on P by A7, A10, A15; :: thesis: verum

end;

end;

end;

end;

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

consider e being Point of (TOP-REAL 2) such that
A19: ( e <> b & e <> c ) and
A20: ( LE b,e,P & LE e,c,P ) by A1, A18, Th8;
take e ; :: thesis: ( e <> b & e <> c & b,e,c,d are_in_this_order_on P )
thus ( e <> b & e <> c ) by A19; :: thesis: b,e,c,d are_in_this_order_on P
LE d,b,P by A17, JORDAN6:58;
hence b,e,c,d are_in_this_order_on P by A20; :: thesis: verum

end;

end;