for L being complete Lattice
for f being monotone UnOp of L
for a being Element of L st a [= f . a holds
ex O being Ordinal st
( card O c= card the carrier of L & (f,O) +. a is_a_fixpoint_of f )