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

proof

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

end;

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