let N1, N2 be Element of Fuzzy_Negations; :: thesis: for NN1, NN2 being Fuzzy_Negation st N1 = NN1 & N2 = NN2 holds
N1 "/\" N2 = min (NN1,NN2)
let NN1, NN2 be Fuzzy_Negation; :: thesis: ( N1 = NN1 & N2 = NN2 implies N1 "/\" N2 = min (NN1,NN2) )
assume A0: ( N1 = NN1 & N2 = NN2 ) ; :: thesis: N1 "/\" N2 = min (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:69;
s "/\" t = min ((@ s),(@ t)) by LFUZZY_0:21;
hence N1 "/\" N2 = min (NN1,NN2) by A0, A4, MinEqMin; :: thesis: verum