theorem :: FUZIMPL4:21

for I being BinOp of [.0,1.]
for N being Fuzzy_Negation st I is N -satisfying_CP holds
( I is satisfying_(LB) iff I is satisfying_(RB) ) by Lemma154iii, Lemma154iv;