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;
per cases ( a = W-min P or a <> W-min P ) ;
suppose A4: a = W-min P ; :: thesis: ex e being Point of (TOP-REAL 2) st
( 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;
suppose A5: a <> W-min P ; :: thesis: ex e being Point of (TOP-REAL 2) st
( a <> e & LE a,e,P )
thus ex e being Point of (TOP-REAL 2) st
( a <> e & LE a,e,P ) :: thesis: verum
proof
per cases ( a in Upper_Arc P or not a in Upper_Arc P ) ;
suppose A6: a in Upper_Arc P ; :: thesis: ex e being Point of (TOP-REAL 2) st
( a <> e & LE a,e,P )
thus ex e being Point of (TOP-REAL 2) st
( a <> e & LE a,e,P ) :: thesis: verum
proof
per cases ( a = E-max P or a <> E-max P ) ;
suppose A7: a = E-max P ; :: thesis: ex e being Point of (TOP-REAL 2) st
( 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;
suppose A9: a <> E-max P ; :: thesis: ex e being Point of (TOP-REAL 2) st
( a <> e & LE a,e,P )
take E-max P ; :: thesis: ( a <> E-max P & LE a, E-max P,P )
E-max P in Lower_Arc P by JORDAN7:1;
hence ( a <> E-max P & LE a, E-max P,P ) by A2, A6, A9, JORDAN6:def 10; :: thesis: verum
end;
end;
end;
end;
suppose A10: not a in Upper_Arc P ; :: thesis: ex e being Point of (TOP-REAL 2) st
( 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;
end;
end;
end;
end;