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