theorem Th28: :: KNASTER:28

for O1 being Ordinal
for L being complete Lattice
for f being monotone UnOp of L
for a being Element of L st a [= f . 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