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

let a, b be Point of (); :: thesis: ( a <> b & LE a,b,P implies ex c being Point of () st
( c <> a & c <> b & LE a,c,P & LE c,b,P ) )

assume that
A1: a <> b and
A2: LE a,b,P ; :: thesis: ex c being Point of () st
( c <> a & c <> b & LE a,c,P & LE c,b,P )

A3: Upper_Arc P is_an_arc_of W-min P, E-max P by JORDAN6:def 8;
A4: Lower_Arc P is_an_arc_of E-max P, W-min P by JORDAN6:def 9;
per cases ( ( a in Upper_Arc P & b in Lower_Arc P & not b = W-min P ) or ( a in Upper_Arc P & b in Upper_Arc P & LE a,b, Upper_Arc P, W-min P, E-max P ) or ( a in Lower_Arc P & b in Lower_Arc P & not b = W-min P & LE a,b, Lower_Arc P, E-max P, W-min P ) ) by ;
suppose that A5: a in Upper_Arc P and
A6: b in Lower_Arc P and
A7: not b = W-min P ; :: thesis: ex c being Point of () st
( c <> a & c <> b & LE a,c,P & LE c,b,P )

A8: E-max P in Lower_Arc P by JORDAN7:1;
A9: ( E-max P in Upper_Arc P & E-max P <> W-min P ) by ;
thus ex c being Point of () st
( c <> a & c <> b & LE a,c,P & LE c,b,P ) :: thesis: verum
proof
per cases ( ( a <> E-max P & b <> E-max P ) or a = E-max P or b = E-max P ) ;
suppose A10: ( a <> E-max P & b <> E-max P ) ; :: thesis: ex c being Point of () st
( c <> a & c <> b & LE a,c,P & LE c,b,P )

take e = E-max P; :: thesis: ( e <> a & e <> b & LE a,e,P & LE e,b,P )
thus ( a <> e & b <> e ) by A10; :: thesis: ( LE a,e,P & LE e,b,P )
thus ( LE a,e,P & LE e,b,P ) by ; :: thesis: verum
end;
suppose A11: a = E-max P ; :: thesis: ex c being Point of () st
( c <> a & c <> b & LE a,c,P & LE c,b,P )

then LE a,b, Lower_Arc P, E-max P, W-min P by ;
then consider e being Point of () such that
A12: ( a <> e & b <> e ) and
A13: ( LE a,e, Lower_Arc P, E-max P, W-min P & LE e,b, Lower_Arc P, E-max P, W-min P ) by A1, A4, Th6;
take e ; :: thesis: ( e <> a & e <> b & LE a,e,P & LE e,b,P )
thus ( e <> a & e <> b ) by A12; :: thesis: ( LE a,e,P & LE e,b,P )
( e in Lower_Arc P & e <> W-min P ) by ;
hence ( LE a,e,P & LE e,b,P ) by ; :: thesis: verum
end;
suppose A14: b = E-max P ; :: thesis: ex c being Point of () st
( c <> a & c <> b & LE a,c,P & LE c,b,P )

then LE a,b, Upper_Arc P, W-min P, E-max P by ;
then consider e being Point of () such that
A15: ( a <> e & b <> e ) and
A16: LE a,e, Upper_Arc P, W-min P, E-max P and
LE e,b, Upper_Arc P, W-min P, E-max P by A1, A3, Th6;
take e ; :: thesis: ( e <> a & e <> b & LE a,e,P & LE e,b,P )
thus ( e <> a & e <> b ) by A15; :: thesis: ( LE a,e,P & LE e,b,P )
e in Upper_Arc P by ;
hence ( LE a,e,P & LE e,b,P ) by ; :: thesis: verum
end;
end;
end;
end;
suppose that A17: ( a in Upper_Arc P & b in Upper_Arc P ) and
A18: LE a,b, Upper_Arc P, W-min P, E-max P ; :: thesis: ex c being Point of () st
( c <> a & c <> b & LE a,c,P & LE c,b,P )

consider e being Point of () such that
A19: ( a <> e & b <> e ) and
A20: LE a,e, Upper_Arc P, W-min P, E-max P and
A21: LE e,b, Upper_Arc P, W-min P, E-max P by A1, A3, A18, Th6;
take e ; :: thesis: ( e <> a & e <> b & LE a,e,P & LE e,b,P )
thus ( e <> a & e <> b ) by A19; :: thesis: ( LE a,e,P & LE e,b,P )
e in Upper_Arc P by ;
hence ( LE a,e,P & LE e,b,P ) by ; :: thesis: verum
end;
suppose that A22: ( a in Lower_Arc P & b in Lower_Arc P ) and
A23: not b = W-min P and
A24: LE a,b, Lower_Arc P, E-max P, W-min P ; :: thesis: ex c being Point of () st
( c <> a & c <> b & LE a,c,P & LE c,b,P )

consider e being Point of () such that
A25: ( a <> e & b <> e ) and
A26: LE a,e, Lower_Arc P, E-max P, W-min P and
A27: LE e,b, Lower_Arc P, E-max P, W-min P by A1, A4, A24, Th6;
take e ; :: thesis: ( e <> a & e <> b & LE a,e,P & LE e,b,P )
thus ( e <> a & e <> b ) by A25; :: thesis: ( LE a,e,P & LE e,b,P )
A28: e in Lower_Arc P by ;
e <> W-min P by ;
hence ( LE a,e,P & LE e,b,P ) by ; :: thesis: verum
end;
end;