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