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