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