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