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