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