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

a in Lower_Arc P

let a be Point of (TOP-REAL 2); :: thesis: ( LE a, W-min P,P implies a in Lower_Arc P )

assume A1: LE a, W-min P,P ; :: thesis: a in Lower_Arc P

a in Lower_Arc P

let a be Point of (TOP-REAL 2); :: thesis: ( LE a, W-min P,P implies a in Lower_Arc P )

assume A1: LE a, W-min P,P ; :: thesis: a in Lower_Arc P

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 A1, JORDAN6:def 10;

end;

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: a in Lower_Arc P

end;

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: a in Lower_Arc P

W-min P in Upper_Arc P and

A3: LE a, W-min P, Upper_Arc P, W-min P, E-max P ; :: thesis: a in Lower_Arc P

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],((TOP-REAL 2) | (Upper_Arc P)), 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 A2, Th1;

thus a in Lower_Arc P :: thesis: verum

end;then consider f being Function of I[01],((TOP-REAL 2) | (Upper_Arc P)), 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 A2, Th1;

thus a in Lower_Arc P :: thesis: verum