let A be non empty set ; :: thesis: for f being monotone UnOp of (BooleLatt A) ex g being V224() Function of (bool A),(bool A) st gfp (A,g) = gfp f

let f be monotone UnOp of (BooleLatt A); :: thesis: ex g being V224() 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 V224() 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; :: thesis: verum

let f be monotone UnOp of (BooleLatt A); :: thesis: ex g being V224() 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 V224() 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; :: thesis: verum