let N be decreasing Fuzzy_Negation; :: thesis: I_RS is N -satisfying_CP
set I = I_RS ;
for x, y being Element of [.0,1.] holds I_RS . (x,y) = I_RS . ((N . y),(N . x))

proof

let x, y be Element of [.0,1.]; :: thesis: I_RS . (x,y) = I_RS . ((N . y),(N . x))

per cases ( x <= y or x > y ) ;

suppose A1: x <= y ; :: thesis: I_RS . (x,y) = I_RS . ((N . y),(N . x))

then A2: N . y <= N . x by FUZIMPL3:7;
I_RS . (x,y) = 1 by A1, FUZIMPL1:def 20
.= I_RS . ((N . y),(N . x)) by A2, FUZIMPL1:def 20 ;
hence I_RS . (x,y) = I_RS . ((N . y),(N . x)) ; :: thesis: verum

end;

suppose A1: x > y ; :: thesis: I_RS . (x,y) = I_RS . ((N . y),(N . x))

then A2: N . x < N . y by FUZIMPL3:8;
I_RS . (x,y) = 0 by A1, FUZIMPL1:def 20
.= I_RS . ((N . y),(N . x)) by A2, FUZIMPL1:def 20 ;
hence I_RS . (x,y) = I_RS . ((N . y),(N . x)) ; :: thesis: verum

end;

end;

end;

hence I_RS is N -satisfying_CP ; :: thesis: verum