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