let P be Simple_closed_curve; :: thesis: for a, b being Point of (TOP-REAL 2) st a <> b & LE a,b,P holds
ex c being Point of (TOP-REAL 2) st
( c <> a & c <> b & LE a,c,P & LE c,b,P )
let a, b be Point of (TOP-REAL 2); :: thesis: ( a <> b & LE a,b,P implies ex c being Point of (TOP-REAL 2) 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 (TOP-REAL 2) 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 A2, JORDAN6:def 10;

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 (TOP-REAL 2) st
( c <> a & c <> b & LE a,c,P & LE c,b,P )

A8: E-max P in Upper_Arc P by JORDAN7:1;
A9: E-max P in Lower_Arc P by JORDAN7:1;
A10: E-max P <> W-min P by TOPREAL5:25;
thus ex c being Point of (TOP-REAL 2) 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 that A11: a <> E-max P and
A12: b <> E-max P ; :: thesis: ex c being Point of (TOP-REAL 2) 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 A11, A12; :: thesis: ( LE a,e,P & LE e,b,P )
thus ( LE a,e,P & LE e,b,P ) by A5, A6, A7, A8, A9, A10, JORDAN6:def 10; :: thesis: verum

end;

suppose A13: a = E-max P ; :: thesis: ex c being Point of (TOP-REAL 2) 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 A4, A6, JORDAN5C:10;
then consider e being Point of (TOP-REAL 2) such that
A14: ( a <> e & b <> e ) and
A15: LE a,e, Lower_Arc P, E-max P, W-min P and
A16: 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 A14; :: thesis: ( LE a,e,P & LE e,b,P )
A17: e in Lower_Arc P by A15, JORDAN5C:def 3;
e <> W-min P by A4, A7, A16, JORDAN6:70;
hence ( LE a,e,P & LE e,b,P ) by A6, A7, A9, A13, A15, A16, A17, JORDAN6:def 10; :: thesis: verum

end;

suppose A18: b = E-max P ; :: thesis: ex c being Point of (TOP-REAL 2) 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 A3, A5, JORDAN5C:10;
then consider e being Point of (TOP-REAL 2) such that
A19: ( a <> e & b <> e ) and
A20: 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 A19; :: thesis: ( LE a,e,P & LE e,b,P )
e in Upper_Arc P by A20, JORDAN5C:def 3;
hence ( LE a,e,P & LE e,b,P ) by A5, A7, A9, A18, A20, JORDAN6:def 10; :: thesis: verum

end;

end;

end;

end;

suppose that A21: a in Upper_Arc P and
A22: b in Upper_Arc P and
A23: LE a,b, Upper_Arc P, W-min P, E-max P ; :: thesis: ex c being Point of (TOP-REAL 2) st
( c <> a & c <> b & LE a,c,P & LE c,b,P )

consider e being Point of (TOP-REAL 2) such that
A24: ( a <> e & b <> e ) and
A25: ( LE a,e, Upper_Arc P, W-min P, E-max P & LE e,b, Upper_Arc P, W-min P, E-max P ) by A1, A3, A23, Th6;
take e ; :: thesis: ( e <> a & e <> b & LE a,e,P & LE e,b,P )
thus ( e <> a & e <> b ) by A24; :: thesis: ( LE a,e,P & LE e,b,P )
e in Upper_Arc P by A25, JORDAN5C:def 3;
hence ( LE a,e,P & LE e,b,P ) by A21, A22, A25, JORDAN6:def 10; :: thesis: verum

end;

suppose that A26: a in Lower_Arc P and
A27: b in Lower_Arc P and
A28: not b = W-min P and
A29: LE a,b, Lower_Arc P, E-max P, W-min P ; :: thesis: ex c being Point of (TOP-REAL 2) st
( c <> a & c <> b & LE a,c,P & LE c,b,P )

consider e being Point of (TOP-REAL 2) such that
A30: ( a <> e & b <> e ) and
A31: LE a,e, Lower_Arc P, E-max P, W-min P and
A32: LE e,b, Lower_Arc P, E-max P, W-min P by A1, A4, A29, Th6;
take e ; :: thesis: ( e <> a & e <> b & LE a,e,P & LE e,b,P )
thus ( e <> a & e <> b ) by A30; :: thesis: ( LE a,e,P & LE e,b,P )
A33: e <> W-min P by A4, A28, A32, JORDAN6:70;
e in Lower_Arc P by A31, JORDAN5C:def 3;
hence ( LE a,e,P & LE e,b,P ) by A26, A27, A28, A31, A32, A33, JORDAN6:def 10; :: thesis: verum

end;

end;