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

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