theorem Lemma154iii: :: FUZIMPL4:13

for I being BinOp of [.0,1.]
for N being Fuzzy_Negation st I is satisfying_(LB) & I is N -satisfying_CP holds
I is satisfying_(RB)