let X be set ; :: thesis: for f being V204() Function of bool X, bool X
for S being Subset of st S c= f . S holds
S c= gfp X,f
let f be V204() Function of bool X, bool X; :: thesis: for S being Subset of st S c= f . S holds
S c= gfp X,f
let S be Subset of ; :: thesis: ( S c= f . S implies S c= gfp X,f )
set H = { h where h is Subset of : h c= f . h } ;
assume S c= f . S ; :: thesis: S c= gfp X,f
then S in { h where h is Subset of : h c= f . h } ;
hence S c= gfp X,f by ZFMISC_1:92; :: thesis: verum