theorem :: WEIERSTR:28

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