let P be Simple_closed_curve; :: thesis: for a being Point of (TOP-REAL 2) st LE a, E-max P,P holds
a in Upper_Arc P
let a be Point of (TOP-REAL 2); :: thesis: ( LE a, E-max P,P implies a in Upper_Arc P )
assume A1: LE a, E-max P,P ; :: thesis: a in Upper_Arc P

per cases ( ( a in Upper_Arc P & E-max P in Lower_Arc P & not E-max P = W-min P ) or ( a in Upper_Arc P & E-max P in Upper_Arc P & LE a, E-max P, Upper_Arc P, W-min P, E-max P ) or ( a in Lower_Arc P & E-max P in Lower_Arc P & not E-max P = W-min P & LE a, E-max P, Lower_Arc P, E-max P, W-min P ) ) by A1, JORDAN6:def 10;

suppose ( ( a in Upper_Arc P & E-max P in Lower_Arc P & not E-max P = W-min P ) or ( a in Upper_Arc P & E-max P in Upper_Arc P & LE a, E-max P, Upper_Arc P, W-min P, E-max P ) ) ; :: thesis: a in Upper_Arc P

hence a in Upper_Arc P ; :: thesis: verum

end;

suppose that A2: a in Lower_Arc P and
( E-max P in Lower_Arc P & not E-max P = W-min P ) and
A3: LE a, E-max P, Lower_Arc P, E-max P, W-min P ; :: thesis: a in Upper_Arc P

Lower_Arc P is_an_arc_of E-max P, W-min P by JORDAN6:def 9;
then consider f being Function of I[01],((TOP-REAL 2) | (Lower_Arc P)), r being Real such that
A4: f is being_homeomorphism and
A5: f . 0 = E-max P and
A6: f . 1 = W-min P and
A7: 0 <= r and
A8: r <= 1 and
A9: f . r = a by A2, Th1;
thus a in Upper_Arc P :: thesis: verum

proof

per cases ( r = 0 or r <> 0 ) ;

suppose r = 0 ; :: thesis: a in Upper_Arc P

hence a in Upper_Arc P by A5, A9, JORDAN7:1; :: thesis: verum

end;

suppose r <> 0 ; :: thesis: a in Upper_Arc P

then r > 0 by A7, XXREAL_0:1;
hence a in Upper_Arc P by A3, A4, A5, A6, A8, A9, JORDAN5C:def 3; :: thesis: verum

end;

end;

end;

end;

end;