theorem Th31: :: PSCOMP_1:31

for p being Point of (TOP-REAL 2)
for Z being non empty Subset of (TOP-REAL 2) st p in W-most Z holds
( p `1 = (W-min Z) `1 & ( Z is compact implies ( (W-min Z) `2 <= p `2 & p `2 <= (W-max Z) `2 ) ) )