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