let P be Simple_closed_curve; :: thesis: for a, b, c, d being Point of () st a <> b & a,b,c,d are_in_this_order_on P holds
ex e being Point of () st
( e <> a & e <> b & a,e,b,c are_in_this_order_on P )

let a, b, c, d be Point of (); :: thesis: ( a <> b & a,b,c,d are_in_this_order_on P implies ex e being Point of () st
( e <> a & e <> b & a,e,b,c 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 () st
( e <> a & e <> b & a,e,b,c 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 () st
( e <> a & e <> b & a,e,b,c are_in_this_order_on P )

then consider e being Point of () such that
A4: ( e <> a & e <> b & LE a,e,P & LE e,b,P ) by ;
take e ; :: thesis: ( e <> a & e <> b & a,e,b,c are_in_this_order_on P )
thus ( e <> a & e <> b & a,e,b,c are_in_this_order_on P ) by A3, A4; :: thesis: verum
end;
suppose that A5: LE b,c,P and
A6: LE c,d,P and
A7: LE d,a,P ; :: thesis: ex e being Point of () st
( e <> a & e <> b & a,e,b,c are_in_this_order_on P )

thus ex e being Point of () st
( e <> a & e <> b & a,e,b,c are_in_this_order_on P ) :: thesis: verum
proof
A8: LE c,a,P by ;
per cases ( b = W-min P or b <> W-min P ) ;
suppose A9: b = W-min P ; :: thesis: ex e being Point of () st
( e <> a & e <> b & a,e,b,c are_in_this_order_on P )

a in P by ;
then consider e being Point of () such that
A10: e <> a and
A11: LE a,e,P by Th7;
take e ; :: thesis: ( e <> a & e <> b & a,e,b,c are_in_this_order_on P )
thus e <> a by A10; :: thesis: ( e <> b & a,e,b,c are_in_this_order_on P )
thus e <> b by ; :: thesis: a,e,b,c are_in_this_order_on P
thus a,e,b,c are_in_this_order_on P by A5, A8, A11; :: thesis: verum
end;
suppose A12: b <> W-min P ; :: thesis: ex e being Point of () st
( e <> a & e <> b & a,e,b,c are_in_this_order_on P )

take e = W-min P; :: thesis: ( e <> a & e <> b & a,e,b,c are_in_this_order_on P )
b in P by ;
then A13: LE e,b,P by JORDAN7:3;
now :: thesis: not e = a
LE b,d,P by ;
then A14: LE b,a,P by ;
assume e = a ; :: thesis: contradiction
hence contradiction by A1, A13, A14, JORDAN6:57; :: thesis: verum
end;
hence e <> a ; :: thesis: ( e <> b & a,e,b,c are_in_this_order_on P )
thus e <> b by A12; :: thesis: a,e,b,c are_in_this_order_on P
thus a,e,b,c are_in_this_order_on P by A5, A8, A13; :: thesis: verum
end;
end;
end;
end;
suppose that A15: LE c,d,P and
A16: ( LE d,a,P & LE a,b,P ) ; :: thesis: ex e being Point of () st
( e <> a & e <> b & a,e,b,c are_in_this_order_on P )

consider e being Point of () such that
A17: ( e <> a & e <> b & LE a,e,P & LE e,b,P ) by A1, A16, Th8;
take e ; :: thesis: ( e <> a & e <> b & a,e,b,c are_in_this_order_on P )
LE c,a,P by ;
hence ( e <> a & e <> b & a,e,b,c are_in_this_order_on P ) by A17; :: thesis: verum
end;
suppose that A18: ( LE d,a,P & LE a,b,P ) and
A19: LE b,c,P ; :: thesis: ex e being Point of () st
( e <> a & e <> b & a,e,b,c are_in_this_order_on P )

consider e being Point of () such that
A20: ( e <> a & e <> b & LE a,e,P & LE e,b,P ) by A1, A18, Th8;
take e ; :: thesis: ( e <> a & e <> b & a,e,b,c are_in_this_order_on P )
thus ( e <> a & e <> b & a,e,b,c are_in_this_order_on P ) by ; :: thesis: verum
end;
end;