:: deftheorem MaxFuz defines max FUZIMPL4:def 9 :
for N1, N2, b₃ being Fuzzy_Negation holds
( b₃ = max (N1,N2) iff ex f, g being Function of [.0,1.],REAL st
( f = N1 & g = N2 & b₃ = max (f,g) ) );