let I be BinOp of [.0,1.]; :: thesis: for N being Fuzzy_Negation st I is satisfying_(I1) & I is N -satisfying_CP holds
I is satisfying_(I2)
let N be Fuzzy_Negation; :: thesis: ( I is satisfying_(I1) & I is N -satisfying_CP implies I is satisfying_(I2) )
assume that
A0: I is satisfying_(I1) and
AA: I is N -satisfying_CP ; :: thesis: I is satisfying_(I2)
for x, y, z being Element of [.0,1.] st y <= z holds
I . (x,y) <= I . (x,z)

proof

let x, y, z be Element of [.0,1.]; :: thesis: ( y <= z implies I . (x,y) <= I . (x,z) )
assume y <= z ; :: thesis: I . (x,y) <= I . (x,z)
then N . z <= N . y by FUZIMPL3:7;
then A1: I . ((N . y),(N . x)) <= I . ((N . z),(N . x)) by A0;
I . (x,y) = I . ((N . y),(N . x)) by AA;
hence I . (x,y) <= I . (x,z) by A1, AA; :: thesis: verum

end;

hence I is satisfying_(I2) ; :: thesis: verum