theorem :: FUZIMPL3:29

for I being satisfying_(EP) satisfying_(OP) BinOp of [.0,1.] holds FNegation I is Fuzzy_Negation ;