let C be Simple_closed_curve; :: thesis: for q being Point of st q in Lower_Arc C & q <> W-min C holds
LE E-max C,q,C
let q be Point of ; :: 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