let D2 be non empty compact non horizontal Subset of (TOP-REAL 2); :: thesis: S-bound D2 < N-bound D2
A1: S-bound D2 <> N-bound D2 by Th16;
S-bound D2 <= N-bound D2 by Th22;
hence S-bound D2 < N-bound D2 by A1, XXREAL_0:1; :: thesis: verum