let X be set ; :: thesis: for f being V224() Function of (bool X),(bool X) holds lfp (X,f) is_a_fixpoint_of f

let f be V224() Function of (bool X),(bool X); :: thesis: lfp (X,f) is_a_fixpoint_of f

defpred S_{1}[ set ] means f . $1 c= $1;

reconsider H = { h where h is Subset of X : S_{1}[h] } as Subset-Family of X from DOMAIN_1:sch 7();

reconsider H = H as Subset-Family of X ;

set A = meet H;

then f . (f . (meet H)) c= f . (meet H) by Def1;

then f . (meet H) in H ;

then meet H c= f . (meet H) by SETFAM_1:3;

hence f . (lfp (X,f)) = lfp (X,f) by A4; :: according to ABIAN:def 4 :: thesis: verum

let f be V224() Function of (bool X),(bool X); :: thesis: lfp (X,f) is_a_fixpoint_of f

defpred S

reconsider H = { h where h is Subset of X : S

reconsider H = H as Subset-Family of X ;

set A = meet H;

now :: thesis: ( H <> {} & ( for h being set st h in H holds

f . (meet H) c= h ) )

then A4:
f . (meet H) c= meet H
by SETFAM_1:5;f . (meet H) c= h ) )

X c= X
;

then reconsider X9 = X as Subset of X ;

f . X9 c= X9 ;

then X9 in H ;

hence H <> {} ; :: thesis: for h being set st h in H holds

f . (meet H) c= h

let h be set ; :: thesis: ( h in H implies f . (meet H) c= h )

assume A1: h in H ; :: thesis: f . (meet H) c= h

then consider x being Subset of X such that

A2: x = h and

A3: f . x c= x ;

meet H c= h by A1, SETFAM_1:3;

then f . (meet H) c= f . x by A2, Def1;

hence f . (meet H) c= h by A2, A3; :: thesis: verum

end;then reconsider X9 = X as Subset of X ;

f . X9 c= X9 ;

then X9 in H ;

hence H <> {} ; :: thesis: for h being set st h in H holds

f . (meet H) c= h

let h be set ; :: thesis: ( h in H implies f . (meet H) c= h )

assume A1: h in H ; :: thesis: f . (meet H) c= h

then consider x being Subset of X such that

A2: x = h and

A3: f . x c= x ;

meet H c= h by A1, SETFAM_1:3;

then f . (meet H) c= f . x by A2, Def1;

hence f . (meet H) c= h by A2, A3; :: thesis: verum

then f . (f . (meet H)) c= f . (meet H) by Def1;

then f . (meet H) in H ;

then meet H c= f . (meet H) by SETFAM_1:3;

hence f . (lfp (X,f)) = lfp (X,f) by A4; :: according to ABIAN:def 4 :: thesis: verum