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