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

now

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

end;

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