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

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

assume W-min P = E-min P ; :: thesis: contradiction
then W-bound P = E-bound P by SPPOL_2:1;
hence contradiction by TOPREAL5:17; :: thesis: verum

end;

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