theorem Th22: :: KNASTER:22

for L being complete Lattice
for f being monotone UnOp of L
for a being Element of L st a [= f . a holds
for O being Ordinal holds a [= (f,O) +. a