theorem :: PSCOMP_1:24

for p being Point of (TOP-REAL 2)
for X being non empty compact Subset of (TOP-REAL 2) st p in X holds
( W-bound X <= p `1 & p `1 <= E-bound X & S-bound X <= p `2 & p `2 <= N-bound X ) by Lm3;