let D1 be non empty compact non vertical Subset of (TOP-REAL 2); :: thesis: W-bound D1 < E-bound D1
A1: W-bound D1 <> E-bound D1 by Th15;
W-bound D1 <= E-bound D1 by Th21;
hence W-bound D1 < E-bound D1 by A1, XXREAL_0:1; :: thesis: verum