:: deftheorem FNeg defines FNegation FUZIMPL3:def 16 :
for I being BinOp of [.0,1.]
for b₂ being UnOp of [.0,1.] holds
( b₂ = FNegation I iff for x being Element of [.0,1.] holds b₂ . x = I . (x,0) );