let C be compact non vertical Subset of (TOP-REAL 2); :: thesis: UMP C <> W-min C
A1: ( (W-min C) `1 = W-bound C & (UMP C) `1 = ((W-bound C) + (E-bound C)) / 2 ) by EUCLID:52;
assume UMP C = W-min C ; :: thesis: contradiction
hence contradiction by A1, SPRECT_1:31; :: thesis: verum