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 X = (dist x) .: P ; :: thesis: X is bounded_below
then for y being real number st y in X holds
0 <= y by Th4;
hence X is bounded_below by SEQ_4:def 2; :: thesis: verum