let M be non empty MetrSpace; :: thesis: 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
let P, Q be non empty Subset of (TopSpaceMetr M); :: thesis: for X being Subset of REAL st X = (dist_max P) .: Q & P is compact & Q is compact holds
X is bounded_above
let X be Subset of REAL; :: thesis: ( X = (dist_max P) .: Q & P is compact & Q is compact implies X is bounded_above )
assume that
A1: X = (dist_max P) .: Q and
A2: ( P is compact & Q is compact ) ; :: thesis: X is bounded_above
reconsider Q9 = Q as non empty Subset of M by TOPMETR:12;
X is bounded_above

proof

take r = max_dist_max (P,Q); :: according to XXREAL_2:def 10 :: thesis: r is UpperBound of X
let p be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( not p in X or p <= r )
assume p in X ; :: thesis: p <= r
then consider z being object such that
z in dom (dist_max P) and
A3: z in Q and
A4: p = (dist_max P) . z by A1, FUNCT_1:def 6;
z in Q9 by A3;
then reconsider z = z as Point of M ;
(dist_max P) . z <= r by A2, A3, Th23;
hence p <= r by A4; :: thesis: verum

end;

hence X is bounded_above ; :: thesis: verum