let L be complete Lattice; :: thesis: for f being monotone UnOp of L holds the carrier of (FixPoints f) c= the carrier of L
let f be monotone UnOp of L; :: thesis: the carrier of (FixPoints f) c= the carrier of L
A1: the carrier of (FixPoints f) = { x where x is Element of L : x is_a_fixpoint_of f } by Th36;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (FixPoints f) or x in the carrier of L )
assume x in the carrier of (FixPoints f) ; :: thesis: x in the carrier of L
then ex a being Element of L st
( x = a & a is_a_fixpoint_of f ) by A1;
hence x in the carrier of L ; :: thesis: verum