let P be Simple_closed_curve; :: thesis: W-max P <> E-max P

now :: thesis: not W-max P = E-max P

A1: |[(E-bound P),(upper_bound (proj2 | (E-most P)))]| = E-max P by PSCOMP_1:def 23;
A2: |[(W-bound P),(upper_bound (proj2 | (W-most P)))]| = W-max P by PSCOMP_1:def 20;
assume W-max P = E-max P ; :: thesis: contradiction
then W-bound P = E-bound P by A2, A1, SPPOL_2:1;
hence contradiction by TOPREAL5:17; :: thesis: verum

end;

hence W-max P <> E-max P ; :: thesis: verum