theorem :: WEIERSTR:25

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_max P) . x1 = upper_bound ((dist_max P) .: Q) ) by Th14, Th24;