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