let P be Simple_closed_curve; :: thesis: LE W-min P, E-max P,P
( W-min P in Upper_Arc P & E-max P in Lower_Arc P & E-max P <> W-min P ) by JORDAN7:1, TOPREAL5:25;
hence LE W-min P, E-max P,P by JORDAN6:def 10; :: thesis: verum