theorem Th4: :: KNASTER:4

for X being set
for f being c=-monotone Function of (bool X),(bool X) holds lfp (X,f) is_a_fixpoint_of f