:: deftheorem Def9 defines min NAGATA_1:def 9 :
for X being set
for r being Real
for f, b₄ being Function of X,REAL holds
( b₄ = min (r,f) iff for x being set st x in X holds
b₄ . x = min (r,(f . x)) );