let I be BinOp of [.0,1.]; :: thesis: for N being Fuzzy_Negation st I is satisfying_(NP) & I is N -satisfying_CP holds
( I is satisfying_(I3) & I is satisfying_(I4) & I is satisfying_(I5) )
let N be Fuzzy_Negation; :: thesis: ( I is satisfying_(NP) & I is N -satisfying_CP implies ( I is satisfying_(I3) & I is satisfying_(I4) & I is satisfying_(I5) ) )
assume that
A1: I is satisfying_(NP) and
A2: I is N -satisfying_CP ; :: thesis: ( I is satisfying_(I3) & I is satisfying_(I4) & I is satisfying_(I5) )
T1: ( N = FNegation I & FNegation I is negation-strong ) by A1, A2, Lemma154va;
0 in [.0,1.] by XXREAL_1:1;
then I . (0,0) = (FNegation I) . 0 by FUZIMPL3:def 16
.= 1 by T1, FUZIMPL3:def 4 ;
hence ( I is satisfying_(I3) & I is satisfying_(I4) & I is satisfying_(I5) ) by A1; :: thesis: verum