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