let C be Simple_closed_curve; :: thesis: for q being Point of (TOP-REAL 2) st q in Upper_Arc C holds
LE q, E-max C,C
let q be Point of (TOP-REAL 2); :: thesis: ( q in Upper_Arc C implies LE q, E-max C,C )
A1: E-max C in Lower_Arc C by JORDAN7:1;
E-max C <> W-min C by TOPREAL5:19;
hence ( q in Upper_Arc C implies LE q, E-max C,C ) by A1, JORDAN6:def 10; :: thesis: verum