let M be non empty MetrSpace; :: thesis: for P being non empty Subset of
for x being Point of
for X being Subset of st X = (dist x) .: P holds
X is bounded_below
let P be non empty Subset of ; :: thesis: for x being Point of
for X being Subset of st X = (dist x) .: P holds
X is bounded_below
let x be Point of ; :: thesis: for X being Subset of st X = (dist x) .: P holds
X is bounded_below
let X be Subset of ; :: 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