theorem Th24: :: KNASTER:24

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