theorem :: FUZIMPL4:31
for f, g being Fuzzy_Negation holds max (f,g) = (maxfuncreal [.0,1.]) . (f,g)