theorem :: PSCOMP_1:66

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