let L be complete Lattice; :: thesis: for f being monotone UnOp of L holds the carrier of (FixPoints f) = { x where x is Element of L : x is_a_fixpoint_of f }

let f be monotone UnOp of L; :: thesis: the carrier of (FixPoints f) = { x where x is Element of L : x is_a_fixpoint_of f }

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 } & FixPoints f = latt P ) by Def9;

hence the carrier of (FixPoints f) = { x where x is Element of L : x is_a_fixpoint_of f } by Def8; :: thesis: verum

let f be monotone UnOp of L; :: thesis: the carrier of (FixPoints f) = { x where x is Element of L : x is_a_fixpoint_of f }

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 } & FixPoints f = latt P ) by Def9;

hence the carrier of (FixPoints f) = { x where x is Element of L : x is_a_fixpoint_of f } by Def8; :: thesis: verum