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 lfp (A,g) = lfp f

let f be monotone UnOp of (BooleLatt A); :: thesis: ex g being V224() Function of (bool A),(bool A) st lfp (A,g) = lfp f

reconsider lf = lfp 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 lg = lfp (A,g) as Element of (BooleLatt A) by LATTICE3:def 1;

take g ; :: thesis: lfp (A,g) = lfp f

lg is_a_fixpoint_of f by Th4;

then lfp f [= lg by Th43;

then A1: lf c= lg by LATTICE3:2;

lfp f is_a_fixpoint_of f by Th41;

then lfp (A,g) c= lf by Th8;

hence lfp (A,g) = lfp 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 lfp (A,g) = lfp f

reconsider lf = lfp 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 lg = lfp (A,g) as Element of (BooleLatt A) by LATTICE3:def 1;

take g ; :: thesis: lfp (A,g) = lfp f

lg is_a_fixpoint_of f by Th4;

then lfp f [= lg by Th43;

then A1: lf c= lg by LATTICE3:2;

lfp f is_a_fixpoint_of f by Th41;

then lfp (A,g) c= lf by Th8;

hence lfp (A,g) = lfp f by A1; :: thesis: verum