let P be Simple_closed_curve; :: thesis: for a being Point of (TOP-REAL 2) st a in P holds

ex e being Point of (TOP-REAL 2) st

( a <> e & LE a,e,P )

let a be Point of (TOP-REAL 2); :: thesis: ( a in P implies ex e being Point of (TOP-REAL 2) st

( a <> e & LE a,e,P ) )

assume A1: a in P ; :: thesis: ex e being Point of (TOP-REAL 2) st

( a <> e & LE a,e,P )

A2: E-max P <> W-min P by TOPREAL5:19;

A3: Lower_Arc P is_an_arc_of E-max P, W-min P by JORDAN6:def 9;

ex e being Point of (TOP-REAL 2) st

( a <> e & LE a,e,P )

let a be Point of (TOP-REAL 2); :: thesis: ( a in P implies ex e being Point of (TOP-REAL 2) st

( a <> e & LE a,e,P ) )

assume A1: a in P ; :: thesis: ex e being Point of (TOP-REAL 2) st

( a <> e & LE a,e,P )

A2: E-max P <> W-min P by TOPREAL5:19;

A3: Lower_Arc P is_an_arc_of E-max P, W-min P by JORDAN6:def 9;

per cases
( a = W-min P or a <> W-min P )
;

end;

suppose A4:
a = W-min P
; :: thesis: ex e being Point of (TOP-REAL 2) st

( a <> e & LE a,e,P )

( a <> e & LE a,e,P )

take
E-max P
; :: thesis: ( a <> E-max P & LE a, E-max P,P )

thus ( a <> E-max P & LE a, E-max P,P ) by A4, JORDAN7:3, SPRECT_1:14, TOPREAL5:19; :: thesis: verum

end;thus ( a <> E-max P & LE a, E-max P,P ) by A4, JORDAN7:3, SPRECT_1:14, TOPREAL5:19; :: thesis: verum

suppose A5:
a <> W-min P
; :: thesis: ex e being Point of (TOP-REAL 2) st

( a <> e & LE a,e,P )

( a <> e & LE a,e,P )

thus
ex e being Point of (TOP-REAL 2) st

( a <> e & LE a,e,P ) :: thesis: verum

end;( a <> e & LE a,e,P ) :: thesis: verum

proof
end;

per cases
( a in Upper_Arc P or not a in Upper_Arc P )
;

end;

suppose A6:
a in Upper_Arc P
; :: thesis: ex e being Point of (TOP-REAL 2) st

( a <> e & LE a,e,P )

( a <> e & LE a,e,P )

thus
ex e being Point of (TOP-REAL 2) st

( a <> e & LE a,e,P ) :: thesis: verum

end;( a <> e & LE a,e,P ) :: thesis: verum

proof
end;

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

end;

suppose A7:
a = E-max P
; :: thesis: ex e being Point of (TOP-REAL 2) st

( a <> e & LE a,e,P )

( a <> e & LE a,e,P )

consider e being Point of (TOP-REAL 2) such that

A8: ( e in Lower_Arc P & e <> E-max P & e <> W-min P ) by A3, JORDAN6:42;

take e ; :: thesis: ( a <> e & LE a,e,P )

thus ( a <> e & LE a,e,P ) by A6, A7, A8, JORDAN6:def 10; :: thesis: verum

end;A8: ( e in Lower_Arc P & e <> E-max P & e <> W-min P ) by A3, JORDAN6:42;

take e ; :: thesis: ( a <> e & LE a,e,P )

thus ( a <> e & LE a,e,P ) by A6, A7, A8, JORDAN6:def 10; :: thesis: verum

suppose A10:
not a in Upper_Arc P
; :: thesis: ex e being Point of (TOP-REAL 2) st

( a <> e & LE a,e,P )

( a <> e & LE a,e,P )

(Upper_Arc P) \/ (Lower_Arc P) = P
by JORDAN6:def 9;

then A11: a in Lower_Arc P by A1, A10, XBOOLE_0:def 3;

then consider f being Function of I[01],((TOP-REAL 2) | (Lower_Arc P)), r being Real such that

A12: f is being_homeomorphism and

A13: f . 0 = E-max P and

A14: f . 1 = W-min P and

A15: 0 <= r and

A16: r <= 1 and

A17: f . r = a by A3, Th1;

A18: f is one-to-one by A12, TOPS_2:def 5;

r < 1 by A5, A14, A16, A17, XXREAL_0:1;

then consider s being Real such that

A19: r < s and

A20: s < 1 by XREAL_1:5;

A21: dom f = [#] I[01] by A12, TOPS_2:def 5

.= [.0,1.] by BORSUK_1:40 ;

A22: rng f = [#] ((TOP-REAL 2) | (Lower_Arc P)) by A12, TOPS_2:def 5

.= the carrier of ((TOP-REAL 2) | (Lower_Arc P))

.= Lower_Arc P by PRE_TOPC:8 ;

A23: 0 <= s by A15, A19, XXREAL_0:2;

then A24: s in dom f by A21, A20, XXREAL_1:1;

then A25: f . s in rng f by FUNCT_1:def 3;

then reconsider e = f . s as Point of (TOP-REAL 2) by A22;

1 in dom f by A21, XXREAL_1:1;

then A26: e <> W-min P by A14, A18, A20, A24, FUNCT_1:def 4;

take e ; :: thesis: ( a <> e & LE a,e,P )

r in dom f by A15, A16, A21, XXREAL_1:1;

hence a <> e by A17, A18, A19, A24, FUNCT_1:def 4; :: thesis: LE a,e,P

LE a,e, Lower_Arc P, E-max P, W-min P by A3, A12, A13, A14, A15, A16, A17, A19, A20, A23, JORDAN5C:8;

hence LE a,e,P by A11, A22, A25, A26, JORDAN6:def 10; :: thesis: verum

end;then A11: a in Lower_Arc P by A1, A10, XBOOLE_0:def 3;

then consider f being Function of I[01],((TOP-REAL 2) | (Lower_Arc P)), r being Real such that

A12: f is being_homeomorphism and

A13: f . 0 = E-max P and

A14: f . 1 = W-min P and

A15: 0 <= r and

A16: r <= 1 and

A17: f . r = a by A3, Th1;

A18: f is one-to-one by A12, TOPS_2:def 5;

r < 1 by A5, A14, A16, A17, XXREAL_0:1;

then consider s being Real such that

A19: r < s and

A20: s < 1 by XREAL_1:5;

A21: dom f = [#] I[01] by A12, TOPS_2:def 5

.= [.0,1.] by BORSUK_1:40 ;

A22: rng f = [#] ((TOP-REAL 2) | (Lower_Arc P)) by A12, TOPS_2:def 5

.= the carrier of ((TOP-REAL 2) | (Lower_Arc P))

.= Lower_Arc P by PRE_TOPC:8 ;

A23: 0 <= s by A15, A19, XXREAL_0:2;

then A24: s in dom f by A21, A20, XXREAL_1:1;

then A25: f . s in rng f by FUNCT_1:def 3;

then reconsider e = f . s as Point of (TOP-REAL 2) by A22;

1 in dom f by A21, XXREAL_1:1;

then A26: e <> W-min P by A14, A18, A20, A24, FUNCT_1:def 4;

take e ; :: thesis: ( a <> e & LE a,e,P )

r in dom f by A15, A16, A21, XXREAL_1:1;

hence a <> e by A17, A18, A19, A24, FUNCT_1:def 4; :: thesis: LE a,e,P

LE a,e, Lower_Arc P, E-max P, W-min P by A3, A12, A13, A14, A15, A16, A17, A19, A20, A23, JORDAN5C:8;

hence LE a,e,P by A11, A22, A25, A26, JORDAN6:def 10; :: thesis: verum