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