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

hereby :: thesis: ( a is_a_fixpoint_of f implies a in the carrier of (FixPoints f) )

assume a in the carrier of (FixPoints f) ; :: thesis: a is_a_fixpoint_of f
then ex b being Element of L st
( a = b & b is_a_fixpoint_of f ) by A1;
hence a is_a_fixpoint_of f ; :: thesis: verum

end;

assume a is_a_fixpoint_of f ; :: thesis: a in the carrier of (FixPoints f)
hence a in the carrier of (FixPoints f) by A1; :: thesis: verum