let N be Fuzzy_Negation; :: thesis: ( N is negation-strict implies N is one-to-one )
assume N is negation-strict ; :: thesis: N is one-to-one
then N is satisfying_(N3) by FUZIMPL3:def 12;
hence N is one-to-one ; :: thesis: verum