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

proof

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

end;

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