let X be set ; :: thesis: for f being V202() 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 V202() 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:92; :: thesis: verum