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

for S being Subset of X st f . S c= S holds

lfp (X,f) c= S

let f be V224() 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