theorem Corr157i: :: FUZIMPL4:20

for I being BinOp of [.0,1.]
for N being Fuzzy_Negation st I is N -satisfying_CP holds
( I is satisfying_(I1) iff I is satisfying_(I2) ) by Lemma154i, Lemma154ii;