let N1, N2 be Element of Fuzzy_Negations; :: thesis: for NN1, NN2 being Fuzzy_Negation st N1 = NN1 & N2 = NN2 holds
N1 "\/" N2 = max (NN1,NN2)
let NN1, NN2 be Fuzzy_Negation; :: thesis: ( N1 = NN1 & N2 = NN2 implies N1 "\/" N2 = max (NN1,NN2) )
assume A0: ( N1 = NN1 & N2 = NN2 ) ; :: thesis: N1 "\/" N2 = max (NN1,NN2)
reconsider s = N1, t = N2 as Element of (FuzzyLattice [.0,1.]) by YELLOW_0:58;
A4: s "\/" t = N1 "\/" N2 by YELLOW_0:70;
s "\/" t = max ((@ s),(@ t)) by LFUZZY_0:19;
hence N1 "\/" N2 = max (NN1,NN2) by A0, A4, MaxEqMax; :: thesis: verum