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