let I be Fuzzy_Implication; 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.]; ( I is satisfying_(NP) implies ConjImpl (I,f) is satisfying_(NP) )
assume B0:
I is satisfying_(NP)
; 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.]; FUZIMPL2:def 1 (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; verum