let L be complete Lattice; for f being monotone UnOp of L holds
( gfp f is_a_fixpoint_of f & ex O being Ordinal st
( card O c= card the carrier of L & (f,O) -. (Top L) = gfp f ) )
let f be monotone UnOp of L; ( gfp f is_a_fixpoint_of f & ex O being Ordinal st
( card O c= card the carrier of L & (f,O) -. (Top L) = gfp f ) )
reconsider je = Top L as Element of L ;
A1:
f . je [= Top L
by LATTICES:19;
then consider O being Ordinal such that
A2:
card O c= card the carrier of L
and
A3:
(f,O) -. (Top L) is_a_fixpoint_of f
by Th31;
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
gfp f is_a_fixpoint_of f
by A1, A3, Th29; ex O being Ordinal st
( card O c= card the carrier of L & (f,O) -. (Top L) = gfp f )
take
O
; ( card O c= card the carrier of L & (f,O) -. (Top L) = gfp f )
thus
card O c= card the carrier of L
by A2; (f,O) -. (Top L) = gfp f
thus
(f,O) -. (Top L) = gfp f
by A1, A3, A4, Th29; verum