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_min 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_min P) .: Q & P is compact & Q is compact holds
X is bounded_above
let X be Subset of REAL ; :: thesis: ( X = (dist_min P) .: Q & P is compact & Q is compact implies X is bounded_above )
assume that
A1: X = (dist_min P) .: Q and
A2: P is compact and
A3: Q is compact ; :: thesis: X is bounded_above
reconsider Q' = 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
A4: ( z in dom (dist_min P) & z in Q & p = (dist_min P) . z ) by A1, FUNCT_1:def 12;
z in Q' by A4;
then reconsider z = z as Point of M ;
(dist_min P) . z <= r by A2, A3, A4, Th24;
hence p <= r by A4; :: thesis: verum

end;

hence X is bounded_above ; :: thesis: verum