set N = N_CC ;
set I = I_LK ;
for x, y being Element of [.0,1.] holds I_LK . (x,y) = I_LK . ((N_CC . y),(N_CC . x))

proof

let x, y be Element of [.0,1.]; :: thesis: I_LK . (x,y) = I_LK . ((N_CC . y),(N_CC . x))
I_LK . (x,y) = min (1,((1 - (1 - y)) + (1 - x))) by FUZIMPL1:def 14
.= min (1,((1 - (N_CC . y)) + (1 - x))) by FUZIMPL3:def 6
.= min (1,((1 - (N_CC . y)) + (N_CC . x))) by FUZIMPL3:def 6
.= I_LK . ((N_CC . y),(N_CC . x)) by FUZIMPL1:def 14 ;
hence I_LK . (x,y) = I_LK . ((N_CC . y),(N_CC . x)) ; :: thesis: verum

end;

hence I_LK is N_CC -satisfying_CP ; :: thesis: verum