theorem Th38: :: KNASTER:38

for L being complete Lattice
for f being monotone UnOp of L
for a being Element of L holds
( a in the carrier of (FixPoints f) iff a is_a_fixpoint_of f )