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

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

proof

A6: LE a,c,P by A3, A4, JORDAN6:73;

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

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

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

end;

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

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

now

assume A12: e = d ; :: thesis: contradiction
LE a,d,P by A5, A6, JORDAN6:73;
hence contradiction by A1, A11, A12, JORDAN6:72; :: thesis: verum

end;

hence e <> d ; :: thesis: ( e <> a & a,c,d,e are_in_this_order_on P )
thus e <> a by A10; :: thesis: a,c,d,e are_in_this_order_on P
thus a,c,d,e are_in_this_order_on P by A5, A6, A11, Def1; :: thesis: verum

end;

end;

end;

end;

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

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

end;

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

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

end;

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

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

end;

end;