let I be BinOp of [.0,1.]; :: thesis: for N being negation-strong Fuzzy_Negation st N = FNegation I & I is N -satisfying_CP holds
I is satisfying_(NP)
let N be negation-strong Fuzzy_Negation; :: thesis: ( N = FNegation I & I is N -satisfying_CP implies I is satisfying_(NP) )
assume A0: N = FNegation I ; :: thesis: ( not I is N -satisfying_CP or I is satisfying_(NP) )
assume A1: I is N -satisfying_CP ; :: thesis: I is satisfying_(NP)
A2: N is involutive by FUZIMPL3:def 13, FUZIMPL3:def 11;
for y being Element of [.0,1.] holds I . (1,y) = y

proof

let y be Element of [.0,1.]; :: thesis: I . (1,y) = y
1 in [.0,1.] by XXREAL_1:1;
then I . (1,y) = I . ((N . y),(N . 1)) by A1
.= I . ((N . y),0) by FUZIMPL3:def 4
.= N . (N . y) by A0, FUZIMPL3:def 16
.= y by A2, FUZIMPL3:def 8 ;
hence I . (1,y) = y ; :: thesis: verum

end;

hence I is satisfying_(NP) by FUZIMPL2:def 1; :: thesis: verum