let P be non empty compact Subset of (TOP-REAL 2); :: thesis: ( P is being_simple_closed_curve implies W-min P <> E-max P )
assume A1: P is being_simple_closed_curve ; :: thesis: W-min P <> E-max P
now :: thesis: not W-min P = E-max P
A2: ( |[(W-bound P),(lower_bound (proj2 | (W-most P)))]| = W-min P & |[(E-bound P),(upper_bound (proj2 | (E-most P)))]| = E-max P ) by PSCOMP_1:def 19, PSCOMP_1:def 23;
assume W-min P = E-max P ; :: thesis: contradiction
then W-bound P = E-bound P by A2, SPPOL_2:1;
hence contradiction by A1, Th17; :: thesis: verum
end;
hence W-min P <> E-max P ; :: thesis: verum