let L be complete Lattice; :: thesis: for f being monotone UnOp of L holds
( lfp f is_a_fixpoint_of f & ex O being Ordinal st
( card O c= card the carrier of L & (f,O) +. (Bottom L) = lfp f ) )
let f be monotone UnOp of L; :: thesis: ( lfp f is_a_fixpoint_of f & ex O being Ordinal st
( card O c= card the carrier of L & (f,O) +. (Bottom L) = lfp f ) )
reconsider ze = Bottom L as Element of L ;
A1: Bottom L [= f . ze by LATTICES:16;
then consider O being Ordinal such that
A2: card O c= card the carrier of L and
A3: (f,O) +. (Bottom L) is_a_fixpoint_of f by Th30;
card the carrier of L in nextcard the carrier of L by CARD_1:def 3;
then card O in nextcard the carrier of L by A2, ORDINAL1:12;
then O in nextcard the carrier of L by CARD_3:44;
then A4: O c= nextcard the carrier of L by ORDINAL1:def 2;
hence lfp f is_a_fixpoint_of f by A1, A3, Th28; :: thesis: ex O being Ordinal st
( card O c= card the carrier of L & (f,O) +. (Bottom L) = lfp f )
take O ; :: thesis: ( card O c= card the carrier of L & (f,O) +. (Bottom L) = lfp f )
thus card O c= card the carrier of L by A2; :: thesis: (f,O) +. (Bottom L) = lfp f
thus (f,O) +. (Bottom L) = lfp f by A1, A3, A4, Th28; :: thesis: verum