theorem :: PSCOMP_1:69

for X being non empty Subset of (TOP-REAL 2)
for Y being compact Subset of (TOP-REAL 2) st X c= Y holds
W-bound X >= W-bound Y by Th16;