let I be BinOp of [.0,1.]; :: thesis: for N being Fuzzy_Negation st I is satisfying_(LB) & I is N -satisfying_CP holds
I is satisfying_(RB)
let N be Fuzzy_Negation; :: thesis: ( I is satisfying_(LB) & I is N -satisfying_CP implies I is satisfying_(RB) )
assume that
A1: I is satisfying_(LB) and
A2: I is N -satisfying_CP ; :: thesis: I is satisfying_(RB)
let x be Element of [.0,1.]; :: according to FUZIMPL1:def 27 :: thesis: I . (x,1) = 1
A3: N . 1 = 0 by FUZIMPL3:def 4;
1 in [.0,1.] by XXREAL_1:1;
then I . (x,1) = I . ((N . 1),(N . x)) by A2
.= 1 by A1, A3 ;
hence I . (x,1) = 1 ; :: thesis: verum