let A be non empty set ; :: thesis: for f being monotone UnOp of (BooleLatt A) ex g being V220() Function of (bool A),(bool A) st gfp (A,g) = gfp f
let f be monotone UnOp of (BooleLatt A); :: thesis: ex g being V220() Function of (bool A),(bool A) st gfp (A,g) = gfp f
reconsider gf = gfp f as Subset of A by LATTICE3:def 1;
the carrier of (BooleLatt A) = bool A by LATTICE3:def 1;
then reconsider g = f as V220() Function of (bool A),(bool A) by Th46;
reconsider gg = gfp (A,g) as Element of (BooleLatt A) by LATTICE3:def 1;
take g ; :: thesis: gfp (A,g) = gfp f
gg is_a_fixpoint_of f by Th5;
then gg [= gfp f by Th43;
then A1: gg c= gf by LATTICE3:2;
gfp f is_a_fixpoint_of f by Th42;
then gf c= gfp (A,g) by Th8;
hence gfp (A,g) = gfp f by A1, XBOOLE_0:def 10; :: thesis: verum