for L being complete Lattice
for f being monotone UnOp of L
for a, b being Element of L st b [= a & b is_a_fixpoint_of f holds
for O2 being Ordinal holds b [= (f,O2) -. a