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