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 Lower_Arc P by JORDAN7:1;
A9: ( E-max P in Upper_Arc P & E-max P <> W-min P ) by JORDAN7:1, TOPREAL5:19;
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 A10: ( a <> E-max P & 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 A10; :: thesis: ( LE a,e,P & LE e,b,P )
thus ( LE a,e,P & LE e,b,P ) by A5, A6, A7, A8, A9, JORDAN6:def 10; :: thesis: verum

end;

suppose A11: 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
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 A4, A7, A13, JORDAN5C:def 3, JORDAN6:55;
hence ( LE a,e,P & LE e,b,P ) by A6, A7, A8, A11, A13, JORDAN6:def 10; :: thesis: verum

end;

suppose A14: 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
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 A16, JORDAN5C:def 3;
hence ( LE a,e,P & LE e,b,P ) by A5, A7, A8, A14, A16, JORDAN6:def 10; :: 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 (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
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 A20, JORDAN5C:def 3;
hence ( LE a,e,P & LE e,b,P ) by A17, A20, A21, JORDAN6:def 10; :: 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 (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
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 A26, JORDAN5C:def 3;
e <> W-min P by A4, A23, A27, JORDAN6:55;
hence ( LE a,e,P & LE e,b,P ) by A22, A23, A26, A27, A28, JORDAN6:def 10; :: thesis: verum

end;

end;