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:16;
X is bounded_above

proof

take r = max_dist_max P,Q; :: according to SEQ_4:def 1 :: thesis: for b₁ being set holds
( not b₁ in X or b₁ <= r )
let p be real number ; :: thesis: ( not p in X or p <= r )
assume p in X ; :: thesis: p <= r
then consider z being set 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 12;
z in Q9 by A3;
then reconsider z = z as Point of M ;
(dist_max P) . z <= r by A2, A3, Th25;
hence p <= r by A4; :: thesis: verum

end;

hence X is bounded_above ; :: thesis: verum