theorem Th25: :: KNASTER:25

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