let C be non empty compact Subset of (TOP-REAL 2); :: thesis: S-bound C <= N-bound C
A1: W-min C in C by Th13;
then A2: (W-min C) `2 <= N-bound C by PSCOMP_1:24;
S-bound C <= (W-min C) `2 by A1, PSCOMP_1:24;
hence S-bound C <= N-bound C by A2, XXREAL_0:2; :: thesis: verum