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

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