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

proof

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

end;

hence I_LK is N_CC -satisfying_L-CP ; :: thesis: verum