for M being non empty MetrSpace
for P, Q being non empty Subset of (TopSpaceMetr M)
for X being Subset of REAL st X = (dist_max P) .: Q & P is compact & Q is compact holds
X is bounded_above