let L be complete Lattice; :: thesis: for f being monotone UnOp of L

for a being Element of L st f . a [= a holds

lfp f [= a

let f be monotone UnOp of L; :: thesis: for a being Element of L st f . a [= a holds

lfp f [= a

let a be Element of L; :: thesis: ( f . a [= a implies lfp f [= a )

assume A1: f . a [= a ; :: thesis: lfp f [= a

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 Th31;

A3: lfp f [= (f,O) -. a by A2, Th43;

(f,O) -. a [= a by A1, Th23;

hence lfp f [= a by A3, LATTICES:7; :: thesis: verum

for a being Element of L st f . a [= a holds

lfp f [= a

let f be monotone UnOp of L; :: thesis: for a being Element of L st f . a [= a holds

lfp f [= a

let a be Element of L; :: thesis: ( f . a [= a implies lfp f [= a )

assume A1: f . a [= a ; :: thesis: lfp f [= a

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 Th31;

A3: lfp f [= (f,O) -. a by A2, Th43;

(f,O) -. a [= a by A1, Th23;

hence lfp f [= a by A3, LATTICES:7; :: thesis: verum