theorem Th12: :: SPRECT_2:12

for X being compact Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in X & p `1 = W-bound X holds
p in W-most X