let X be set ; :: thesis: for f being c=-monotone Function of (bool X),(bool X) holds gfp (X,f) is_a_fixpoint_of f
let f be c=-monotone Function of (bool X),(bool X); :: thesis: gfp (X,f) is_a_fixpoint_of f
defpred S₁[ set ] means $1 c= f . $1;
reconsider H = { h where h is Subset of X : S₁[h] } as Subset-Family of X from DOMAIN_1:sch 7();
set A = union H;

now :: thesis: for x being set st x in H holds
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;

then A4: union H c= f . (union H) by ZFMISC_1:76;
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