:: deftheorem defines gfp KNASTER:def 3 :
for X being set
for f being c=-monotone Function of (bool X),(bool X) holds gfp (X,f) = union { h where h is Subset of X : h c= f . h } ;