theorem :: FUZIMPL4:3

for N1, N2 being Fuzzy_Negation st N1 ~ = N2 holds
N1 is one-to-one by LemmaOne;