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;

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;

end;

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 )

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

end;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
end;

per cases
( ( a <> E-max P & b <> E-max P ) or a = E-max P or b = E-max P )
;

end;

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 )

( 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;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

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 )

( 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;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

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 )

( 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;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

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 )

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;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

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 )

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;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