let C be compact non vertical Subset of (TOP-REAL 2); :: thesis: UMP C <> E-max C
assume A1: UMP C = E-max C ; :: thesis: contradiction
A2: (E-max C) `1 = E-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