:: deftheorem defines satisfying_(NP) FUZIMPL2:def 1 :
for I being BinOp of [.0,1.] holds
( I is satisfying_(NP) iff for y being Element of [.0,1.] holds I . (1,y) = y );