theorem Th32: :: KNASTER:32

for L being complete Lattice
for f being monotone UnOp of L
for a, b being Element of L st a is_a_fixpoint_of f & b is_a_fixpoint_of f holds
ex O being Ordinal st
( card O c= card the carrier of L & (f,O) +. (a "\/" b) is_a_fixpoint_of f & a [= (f,O) +. (a "\/" b) & b [= (f,O) +. (a "\/" b) )