let P be Simple_closed_curve; :: thesis: for a being Point of () st LE a, W-min P,P holds
a in Lower_Arc P

let a be Point of (); :: thesis: ( LE a, W-min P,P implies a in Lower_Arc P )
assume A1: LE a, W-min P,P ; :: thesis:
per cases ( ( a in Upper_Arc P & W-min P in Lower_Arc P & not W-min P = W-min P ) or ( a in Lower_Arc P & W-min P in Lower_Arc P & not W-min P = W-min P & LE a, W-min P, Lower_Arc P, E-max P, W-min P ) or ( a in Upper_Arc P & W-min P in Upper_Arc P & LE a, W-min P, Upper_Arc P, W-min P, E-max P ) ) by ;
suppose ( ( a in Upper_Arc P & W-min P in Lower_Arc P & not W-min P = W-min P ) or ( a in Lower_Arc P & W-min P in Lower_Arc P & not W-min P = W-min P & LE a, W-min P, Lower_Arc P, E-max P, W-min P ) ) ; :: thesis:
end;
suppose that A2: a in Upper_Arc P and
W-min P in Upper_Arc P and
A3: LE a, W-min P, Upper_Arc P, W-min P, E-max P ; :: thesis:
Upper_Arc P is_an_arc_of W-min P, E-max P by JORDAN6:def 8;
then consider f being Function of I[01],(() | ()), r being Real such that
A4: f is being_homeomorphism and
A5: f . 0 = W-min P and
A6: f . 1 = E-max P and
A7: 0 <= r and
A8: r <= 1 and
A9: f . r = a by ;
thus a in Lower_Arc P :: thesis: verum
end;
end;