theorem Th27: :: KNASTER:27

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 & not (f,O2) -. a is_a_fixpoint_of f holds
(f,O1) -. a <> (f,O2) -. a