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 holds
X is bounded_below
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 holds
X is bounded_below
let x be Point of M; :: thesis: for X being Subset of REAL st X = (dist x) .: P holds
X is bounded_below
let X be Subset of REAL; :: thesis: ( X = (dist x) .: P implies X is bounded_below )
assume A1: X = (dist x) .: P ; :: thesis: X is bounded_below
take 0 ; :: according to XXREAL_2:def 9 :: thesis: 0 is LowerBound of X
let y be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( not y in X or 0 <= y )
thus ( y in X implies 0 <= y ) by A1, Th4; :: thesis: verum