theorem :: WEIERSTR:17

for M being non empty MetrSpace
for x being Point of M
for P being Subset of (TopSpaceMetr M) st P <> {} & P is compact holds
ex x1 being Point of (TopSpaceMetr M) st
( x1 in P & (dist x) . x1 = upper_bound ((dist x) .: P) ) by Th14, Th16;