let L be complete Lattice; :: thesis: for f being monotone UnOp of L
for a being Element of L st a [= f . a holds
a [= gfp f
let f be monotone UnOp of L; :: thesis: for a being Element of L st a [= f . a holds
a [= gfp f
let a be Element of L; :: thesis: ( a [= f . a implies a [= gfp f )
assume A1: a [= f . a ; :: thesis: a [= gfp f
then consider O being Ordinal such that
card O c= card the carrier of L and
A2: (f,O) +. a is_a_fixpoint_of f by Th30;
A3: (f,O) +. a [= gfp f by A2, Th43;
a [= (f,O) +. a by A1, Th22;
hence a [= gfp f by A3, LATTICES:7; :: thesis: verum