let I be Fuzzy_Implication; :: thesis: for f being bijective increasing UnOp of [.0,1.] st I is satisfying_(EP) holds
ConjImpl (I,f) is satisfying_(EP)
let f be bijective increasing UnOp of [.0,1.]; :: thesis: ( I is satisfying_(EP) implies ConjImpl (I,f) is satisfying_(EP) )
assume B0: I is satisfying_(EP) ; :: thesis: ConjImpl (I,f) is satisfying_(EP)
set g = ConjImpl (I,f);
let x, y, z be Element of [.0,1.]; :: according to FUZIMPL2:def 2 :: thesis: (ConjImpl (I,f)) . (x,((ConjImpl (I,f)) . (y,z))) = (ConjImpl (I,f)) . (y,((ConjImpl (I,f)) . (x,z)))
I . ((f . y),(f . z)) in [.0,1.] ;
then BB: I . ((f . y),(f . z)) in rng f by FUNCT_2:def 3;
I . ((f . x),(f . z)) in [.0,1.] ;
then B2: I . ((f . x),(f . z)) in rng f by FUNCT_2:def 3;
(ConjImpl (I,f)) . (x,((ConjImpl (I,f)) . (y,z))) = (ConjImpl (I,f)) . (x,((f ") . (I . ((f . y),(f . z))))) by BIDef
.= (f ") . (I . ((f . x),(f . ((f ") . (I . ((f . y),(f . z))))))) by BIDef
.= (f ") . (I . ((f . x),(I . ((f . y),(f . z))))) by FUNCT_1:35, BB
.= (f ") . (I . ((f . y),(I . ((f . x),(f . z))))) by B0, FUZIMPL2:def 2
.= (f ") . (I . ((f . y),(f . ((f ") . (I . ((f . x),(f . z))))))) by B2, FUNCT_1:35
.= (ConjImpl (I,f)) . (y,((f ") . (I . ((f . x),(f . z))))) by BIDef
.= (ConjImpl (I,f)) . (y,((ConjImpl (I,f)) . (x,z))) by BIDef ;
hence (ConjImpl (I,f)) . (x,((ConjImpl (I,f)) . (y,z))) = (ConjImpl (I,f)) . (y,((ConjImpl (I,f)) . (x,z))) ; :: thesis: verum