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