let L be complete Lattice; :: thesis: 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; :: thesis: ( 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; :: thesis: ex O being Ordinal st

( card O c= card the carrier of L & (f,O) -. (Top L) = gfp f )

take O ; :: thesis: ( 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; :: thesis: (f,O) -. (Top L) = gfp f

thus (f,O) -. (Top L) = gfp f by A1, A3, A4, Th29; :: thesis: verum

( 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; :: thesis: ( 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; :: thesis: ex O being Ordinal st

( card O c= card the carrier of L & (f,O) -. (Top L) = gfp f )

take O ; :: thesis: ( 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; :: thesis: (f,O) -. (Top L) = gfp f

thus (f,O) -. (Top L) = gfp f by A1, A3, A4, Th29; :: thesis: verum