:: deftheorem DEFM1 defines min COUSIN2:def 1 :
for X being non empty set
for f, g, b₄ being Function of X,REAL holds
( b₄ = min (f,g) iff for x being Element of X holds b₄ . x = min ((f . x),(g . x)) );