let I be Fuzzy_Implication; :: thesis: for f being bijective increasing UnOp of [.0,1.] st I is satisfying_(IP) holds
ConjImpl (I,f) is satisfying_(IP)
let f be bijective increasing UnOp of [.0,1.]; :: thesis: ( I is satisfying_(IP) implies ConjImpl (I,f) is satisfying_(IP) )
assume B0: I is satisfying_(IP) ; :: thesis: ConjImpl (I,f) is satisfying_(IP)
set g = ConjImpl (I,f);
let x be Element of [.0,1.]; :: according to FUZIMPL2:def 3 :: thesis: (ConjImpl (I,f)) . (x,x) = 1
(ConjImpl (I,f)) . (x,x) = (f ") . (I . ((f . x),(f . x))) by BIDef
.= (f ") . 1 by FUZIMPL2:def 3, B0
.= 1 by LemmaBound ;
hence (ConjImpl (I,f)) . (x,x) = 1 ; :: thesis: verum