theorem :: KNASTER:40

for L being complete Lattice
for f being monotone UnOp of L holds FixPoints f is complete