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

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

hence
W-min P <> E-min P
; :: thesis: verumassume
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;then W-bound P = E-bound P by SPPOL_2:1;

hence contradiction by TOPREAL5:17; :: thesis: verum