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