let X be set ; :: thesis: for f being V197 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 V197 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