:: deftheorem Def9 defines FixPoints KNASTER:def 9 :
for L being complete Lattice
for f being UnOp of L st f is monotone holds
for b₃ being strict Lattice holds
( b₃ = FixPoints f iff ex P being non empty with_suprema with_infima Subset of L st
( P = { x where x is Element of L : x is_a_fixpoint_of f } & b₃ = latt P ) );