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

for S being Subset of X st S c= f . S holds

S c= gfp (X,f)

let f be V224() Function of (bool X),(bool X); :: thesis: for S being Subset of X st S c= f . S holds

S c= gfp (X,f)

let S be Subset of X; :: thesis: ( S c= f . S implies S c= gfp (X,f) )

set H = { h where h is Subset of X : h c= f . h } ;

assume S c= f . S ; :: thesis: S c= gfp (X,f)

then S in { h where h is Subset of X : h c= f . h } ;

hence S c= gfp (X,f) by ZFMISC_1:74; :: thesis: verum

for S being Subset of X st S c= f . S holds

S c= gfp (X,f)

let f be V224() Function of (bool X),(bool X); :: thesis: for S being Subset of X st S c= f . S holds

S c= gfp (X,f)

let S be Subset of X; :: thesis: ( S c= f . S implies S c= gfp (X,f) )

set H = { h where h is Subset of X : h c= f . h } ;

assume S c= f . S ; :: thesis: S c= gfp (X,f)

then S in { h where h is Subset of X : h c= f . h } ;

hence S c= gfp (X,f) by ZFMISC_1:74; :: thesis: verum