theorem Th21: :: KNASTER:21

for L being complete Lattice
for f being monotone UnOp of L ex a being Element of L st a is_a_fixpoint_of f