theorem Th23: :: KNASTER:23

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