let I be BinOp of [.0,1.]; :: thesis: for N being Fuzzy_Negation st I is satisfying_(NP) & I is N -satisfying_CP holds
( N = FNegation I & FNegation I is negation-strong )
let N be Fuzzy_Negation; :: thesis: ( I is satisfying_(NP) & I is N -satisfying_CP implies ( N = FNegation I & FNegation I is negation-strong ) )
assume that
A1: I is satisfying_(NP) and
A2: I is N -satisfying_CP ; :: thesis: ( N = FNegation I & FNegation I is negation-strong )
set NI = FNegation I;
A3: N . 0 = 1 by FUZIMPL3:def 4;
B1: 0 in [.0,1.] by XXREAL_1:1;
B2: 1 in [.0,1.] by XXREAL_1:1;
for x being Element of [.0,1.] holds (FNegation I) . x = N . x

proof

let x be Element of [.0,1.]; :: thesis: (FNegation I) . x = N . x
(FNegation I) . x = I . (x,0) by FUZIMPL3:def 16
.= I . ((N . 0),(N . x)) by B1, A2
.= N . x by A1, A3, FUZIMPL2:def 1 ;
hence (FNegation I) . x = N . x ; :: thesis: verum

end;

hence T1: N = FNegation I by FUNCT_2:63; :: thesis: FNegation I is negation-strong
then C1: (FNegation I) . 1 = 0 by FUZIMPL3:def 4;
for y being Element of [.0,1.] holds y = (FNegation I) . ((FNegation I) . y)

proof

let y be Element of [.0,1.]; :: thesis: y = (FNegation I) . ((FNegation I) . y)
y = I . (1,y) by A1, FUZIMPL2:def 1
.= I . (((FNegation I) . y),((FNegation I) . 1)) by B2, A2, T1
.= (FNegation I) . ((FNegation I) . y) by C1, FUZIMPL3:def 16 ;
hence y = (FNegation I) . ((FNegation I) . y) ; :: thesis: verum

end;

then FNegation I is involutive by FUZIMPL3:def 8;
hence FNegation I is negation-strong by FUZIMPL3:def 13, FUZIMPL3:def 11; :: thesis: verum