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