for x being Element of [.0,1.] holds N_CC . (N_CC . x) = x

proof

let x be Element of [.0,1.]; :: thesis: N_CC . (N_CC . x) = x
A1: 1 - x in [.0,1.] by FUZNORM1:7;
N_CC . (N_CC . x) = N_CC . (1 - x) by FUZIMPL3:def 6
.= 1 - (1 - x) by A1, FUZIMPL3:def 6
.= x ;
hence N_CC . (N_CC . x) = x ; :: thesis: verum

end;

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