let P be Subset of (TOP-REAL 2); :: thesis: for q being Point of (TOP-REAL 2) st P is being_simple_closed_curve & q in P holds
LE q,q,P
let q be Point of (TOP-REAL 2); :: thesis: ( P is being_simple_closed_curve & q in P implies LE q,q,P )
assume A1: ( P is being_simple_closed_curve & q in P ) ; :: thesis: LE q,q,P
then A2: ( Lower_Arc P is_an_arc_of E-max P, W-min P & (Upper_Arc P) /\ (Lower_Arc P) = {(W-min P),(E-max P)} & (Upper_Arc P) \/ (Lower_Arc P) = P & (First_Point (Upper_Arc P),(W-min P),(E-max P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 > (Last_Point (Lower_Arc P),(E-max P),(W-min P),(Vertical_Line (((W-bound P) + (E-bound P)) / 2))) `2 ) by Def9;
A3: Upper_Arc P is_an_arc_of W-min P, E-max P by A1, Th65;

now

per cases ( q in Upper_Arc P or ( q in Lower_Arc P & not q in Upper_Arc P ) ) by A1, A2, XBOOLE_0:def 3;

case A4: q in Upper_Arc P ; :: thesis: LE q,q,P

then LE q,q, Upper_Arc P, W-min P, E-max P by JORDAN5C:9;
hence LE q,q,P by A4, Def10; :: thesis: verum

end;

case A5: ( q in Lower_Arc P & not q in Upper_Arc P ) ; :: thesis: LE q,q,P

then A6: LE q,q, Lower_Arc P, E-max P, W-min P by JORDAN5C:9;
q <> W-min P by A3, A5, TOPREAL1:4;
hence LE q,q,P by A5, A6, Def10; :: thesis: verum

end;

end;

end;

hence LE q,q,P ; :: thesis: verum