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

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

end;

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

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

proof

A9: LE b,d,P by A6, A7, JORDAN6:58;

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

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

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

end;

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

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

now :: thesis: not e = a

LE b,d,P by A6, A7, JORDAN6:58;
then A15: LE b,a,P by A8, JORDAN6:58;
assume e = a ; :: thesis: contradiction
hence contradiction by A1, A14, A15, JORDAN6:57; :: thesis: verum

end;

hence e <> a ; :: thesis: ( e <> b & a,e,b,d are_in_this_order_on P )
thus e <> b by A13; :: thesis: a,e,b,d are_in_this_order_on P
thus a,e,b,d are_in_this_order_on P by A8, A9, A14; :: thesis: verum

end;

end;

end;

end;

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

consider e being Point of (TOP-REAL 2) such that
A18: ( e <> a & e <> b & LE a,e,P & LE e,b,P ) by A1, A17, Th8;
take e ; :: thesis: ( e <> a & e <> b & a,e,b,d are_in_this_order_on P )
thus ( e <> a & e <> b & a,e,b,d are_in_this_order_on P ) by A16, A18; :: thesis: verum

end;

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

consider e being Point of (TOP-REAL 2) such that
A21: ( e <> a & e <> b & LE a,e,P & LE e,b,P ) by A1, A20, Th8;
take e ; :: thesis: ( e <> a & e <> b & a,e,b,d are_in_this_order_on P )
thus ( e <> a & e <> b & a,e,b,d are_in_this_order_on P ) by A19, A21; :: thesis: verum

end;

end;