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:25;
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 )
E-max P in P by SPRECT_1:16;
hence ( a <> E-max P & LE a, E-max P,P ) by A4, JORDAN7:3, TOPREAL5:25; :: 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:55;
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: dom f = [#] I[01] by A12, TOPS_2:def 5
.= [.0 ,1.] by BORSUK_1:83 ;
then A19: r in dom f by A15, A16, XXREAL_1:1;
A20: 1 in dom f by A18, XXREAL_1:1;
A21: 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 number such that
A22: ( r < s & s < 1 ) by XREAL_1:7;
A23: s is Real by XREAL_0:def 1;
A24: ( 0 <= s & s <= 1 ) by A15, A22, XXREAL_0:2;
then A25: s in dom f by A18, XXREAL_1:1;
A26: 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:29 ;
A27: f . s in rng f by A25, FUNCT_1:def 5;
then reconsider e = f . s as Point of (TOP-REAL 2) by A26;
take e ; :: thesis: ( a <> e & LE a,e,P )
thus a <> e by A17, A19, A21, A22, A25, FUNCT_1:def 8; :: thesis: LE a,e,P
A28: e <> W-min P by A14, A20, A21, A22, A25, FUNCT_1:def 8;
LE a,e, Lower_Arc P, E-max P, W-min P by A3, A12, A13, A14, A15, A16, A17, A22, A23, A24, JORDAN5C:8;
hence LE a,e,P by A11, A26, A27, A28, JORDAN6:def 10; :: thesis: verum
end;
end;
end;
end;
end;