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;

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

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 is_a_fixpoint_of f
; :: thesis: 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;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

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