:: deftheorem Def3 defines lower_bound NAGATA_2:def 3 :
for X being non empty set
for f being Function of [:X,X:],REAL
for A being Subset of X
for b₄ being Function of X,REAL holds
( b₄ = lower_bound (f,A) iff for x being Element of X holds b₄ . x = lower_bound ((dist (f,x)) .: A) );