theorem Th8: :: KNASTER:8

for X being set
for f being c=-monotone 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) ) by Th6, Th7;