let X be set ; :: thesis: for f being V224() Function of (bool X),(bool X) holds gfp (X,f) is_a_fixpoint_of f

let f be V224() Function of (bool X),(bool X); :: thesis: gfp (X,f) is_a_fixpoint_of f

defpred S_{1}[ set ] means $1 c= f . $1;

reconsider H = { h where h is Subset of X : S_{1}[h] } as Subset-Family of X from DOMAIN_1:sch 7();

set A = union H;

then f . (union H) c= f . (f . (union H)) by Def1;

then f . (union H) in H ;

then f . (union H) c= union H by ZFMISC_1:74;

hence f . (gfp (X,f)) = gfp (X,f) by A4; :: according to ABIAN:def 4 :: thesis: verum

let f be V224() Function of (bool X),(bool X); :: thesis: gfp (X,f) is_a_fixpoint_of f

defpred S

reconsider H = { h where h is Subset of X : S

set A = union H;

now :: thesis: for x being set st x in H holds

x c= f . (union H)

then A4:
union H c= f . (union H)
by ZFMISC_1:76;x c= f . (union H)

let x be set ; :: thesis: ( x in H implies x c= f . (union H) )

assume A1: x in H ; :: thesis: x c= f . (union H)

then consider h being Subset of X such that

A2: x = h and

A3: h c= f . h ;

h c= union H by A1, A2, ZFMISC_1:74;

then f . h c= f . (union H) by Def1;

hence x c= f . (union H) by A2, A3; :: thesis: verum

end;assume A1: x in H ; :: thesis: x c= f . (union H)

then consider h being Subset of X such that

A2: x = h and

A3: h c= f . h ;

h c= union H by A1, A2, ZFMISC_1:74;

then f . h c= f . (union H) by Def1;

hence x c= f . (union H) by A2, A3; :: thesis: verum

then f . (union H) c= f . (f . (union H)) by Def1;

then f . (union H) in H ;

then f . (union H) c= union H by ZFMISC_1:74;

hence f . (gfp (X,f)) = gfp (X,f) by A4; :: according to ABIAN:def 4 :: thesis: verum