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