theorem Th36: :: KNASTER:36

for L being complete Lattice
for f being monotone UnOp of L holds the carrier of (FixPoints f) = { x where x is Element of L : x is_a_fixpoint_of f }