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