let X be set ; :: thesis: for f being V204() Function of (bool X),(bool X)
for S being Subset of X st S is_a_fixpoint_of f holds
( lfp (X,f) c= S & S c= gfp (X,f) )
let f be V204() Function of (bool X),(bool X); :: thesis: for S being Subset of X st S is_a_fixpoint_of f holds
( lfp (X,f) c= S & S c= gfp (X,f) )
let S be Subset of X; :: thesis: ( S is_a_fixpoint_of f implies ( lfp (X,f) c= S & S c= gfp (X,f) ) )
assume S = f . S ; :: according to ABIAN:def 4 :: thesis: ( lfp (X,f) c= S & S c= gfp (X,f) )
hence ( lfp (X,f) c= S & S c= gfp (X,f) ) by Th8, Th9; :: thesis: verum