theorem :: PSCOMP_1:67

for X being non empty Subset of (TOP-REAL 2)
for Y being compact Subset of (TOP-REAL 2) st X c= Y holds
E-bound X <= E-bound Y by Th17;