let X be set ; :: thesis: for f being V204() Function of bool X, bool X
for S being Subset of 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 st S is_a_fixpoint_of f holds
( lfp X,f c= S & S c= gfp X,f )
let S be Subset of ; :: 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