let M be non empty MetrSpace; :: thesis: for P being non empty Subset of (TopSpaceMetr M)
for x being Point of M
for X being Subset of REAL st X = (dist x) .: P & P is compact holds
X is bounded_above
let P be non empty Subset of (TopSpaceMetr M); :: thesis: for x being Point of M
for X being Subset of REAL st X = (dist x) .: P & P is compact holds
X is bounded_above
let x be Point of M; :: thesis: for X being Subset of REAL st X = (dist x) .: P & P is compact holds
X is bounded_above
let X be Subset of REAL; :: thesis: ( X = (dist x) .: P & P is compact implies X is bounded_above )
assume ( X = (dist x) .: P & P is compact ) ; :: thesis: X is bounded_above
then ( [#] ((dist x) .: P) is real-bounded & X = [#] ((dist x) .: P) ) by WEIERSTR:9, WEIERSTR:11, WEIERSTR:def 1;
hence X is bounded_above ; :: thesis: verum