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

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

hence
W-max P <> E-max P
; :: thesis: verumA1:
|[(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;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