:: deftheorem D2Def defines NegationD2 FUZIMPL3:def 18 :
for b₁ being UnOp of [.0,1.] holds
( b₁ = NegationD2 iff for x being Element of [.0,1.] holds
( ( x = 1 implies b₁ . x = 0 ) & ( x <> 1 implies b₁ . x = 1 ) ) );