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 Th34;
A3: lfp f [= f,O -. a by A2, Th46;
f,O -. a [= a by A1, Th26;
hence lfp f [= a by A3, LATTICES:25; :: thesis: verum