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

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