:: deftheorem FuzNegDef defines Fuzzy_Negations FUZIMPL4:def 11 :
for b₁ being strict full SubRelStr of FuzzyLattice [.0,1.] holds
( b₁ = Fuzzy_Negations iff the carrier of b₁ = { f where f is Fuzzy_Negation : verum } );