let P be Simple_closed_curve; :: thesis: for a being Point of () st a in P holds
ex e being Point of () st
( a <> e & LE a,e,P )

let a be Point of (); :: thesis: ( a in P implies ex e being Point of () st
( a <> e & LE a,e,P ) )

assume A1: a in P ; :: thesis: ex e being Point of () 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 () 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 ; :: thesis: verum
end;
suppose A5: a <> W-min P ; :: thesis: ex e being Point of () st
( a <> e & LE a,e,P )

thus ex e being Point of () 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 () st
( a <> e & LE a,e,P )

thus ex e being Point of () 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 () st
( a <> e & LE a,e,P )

consider e being Point of () such that
A8: ( e in Lower_Arc P & e <> E-max P & e <> W-min P ) by ;
take e ; :: thesis: ( a <> e & LE a,e,P )
thus ( a <> e & LE a,e,P ) by ; :: thesis: verum
end;
suppose A9: a <> E-max P ; :: thesis: ex e being Point of () 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 ; :: thesis: verum
end;
end;
end;
end;
suppose A10: not a in Upper_Arc P ; :: thesis: ex e being Point of () st
( a <> e & LE a,e,P )

(Upper_Arc P) \/ () = P by JORDAN6:def 9;
then A11: a in Lower_Arc P by ;
then consider f being Function of I,(() | ()), 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 ;
A18: f is one-to-one by ;
r < 1 by ;
then consider s being Real such that
A19: r < s and
A20: s < 1 by XREAL_1:5;
A21: dom f = [#] I by
.= [.0,1.] by BORSUK_1:40 ;
A22: rng f = [#] (() | ()) by
.= the carrier of (() | ())
.= Lower_Arc P by PRE_TOPC:8 ;
A23: 0 <= s by ;
then A24: s in dom f by ;
then A25: f . s in rng f by FUNCT_1:def 3;
then reconsider e = f . s as Point of () by A22;
1 in dom f by ;
then A26: e <> W-min P by ;
take e ; :: thesis: ( a <> e & LE a,e,P )
r in dom f by ;
hence a <> e by ; :: 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 ; :: thesis: verum
end;
end;
end;
end;
end;