let I be Fuzzy_Implication; :: thesis: for f being bijective increasing UnOp of [.0,1.] st I is satisfying_(OP) holds
ConjImpl (I,f) is satisfying_(OP)
let f be bijective increasing UnOp of [.0,1.]; :: thesis: ( I is satisfying_(OP) implies ConjImpl (I,f) is satisfying_(OP) )
assume B0: I is satisfying_(OP) ; :: thesis: ConjImpl (I,f) is satisfying_(OP)
set g = ConjImpl (I,f);
let x, y be Element of [.0,1.]; :: according to FUZIMPL2:def 4 :: thesis: ( ( not (ConjImpl (I,f)) . (x,y) = 1 or x <= y ) & ( not x <= y or (ConjImpl (I,f)) . (x,y) = 1 ) )
b3: rng f = [.0,1.] by FUNCT_2:def 3;
b4: dom f = [.0,1.] by FUNCT_2:def 1;
thus ( (ConjImpl (I,f)) . (x,y) = 1 implies x <= y ) :: thesis: ( not x <= y or (ConjImpl (I,f)) . (x,y) = 1 )

proof

assume (ConjImpl (I,f)) . (x,y) = 1 ; :: thesis: x <= y
then (f ") . (I . ((f . x),(f . y))) = 1 by BIDef;
then f . ((f ") . (I . ((f . x),(f . y)))) = 1 by LemmaBound;
then I . ((f . x),(f . y)) = 1 by FUNCT_1:35, b3;
then f . x <= f . y by FUZIMPL2:def 4, B0;
then (f ") . (f . x) <= (f ") . (f . y) by Rosnie;
then x <= (f ") . (f . y) by b4, FUNCT_1:34;
hence x <= y by b4, FUNCT_1:34; :: thesis: verum

end;

assume x <= y ; :: thesis: (ConjImpl (I,f)) . (x,y) = 1
then f . x <= f . y by Rosnie;
then I . ((f . x),(f . y)) = 1 by FUZIMPL2:def 4, B0;
then (f ") . (I . ((f . x),(f . y))) = 1 by LemmaBound;
hence (ConjImpl (I,f)) . (x,y) = 1 by BIDef; :: thesis: verum