let L be complete Lattice; for f being monotone UnOp of L
for a being Element of L st f . a [= a holds
ex O being Ordinal st
( card O c= card the carrier of L & (f,O) -. a is_a_fixpoint_of f )
let f be monotone UnOp of L; for a being Element of L st f . a [= a holds
ex O being Ordinal st
( card O c= card the carrier of L & (f,O) -. a is_a_fixpoint_of f )
let a be Element of L; ( f . a [= a implies ex O being Ordinal st
( card O c= card the carrier of L & (f,O) -. a is_a_fixpoint_of f ) )
set cL = the carrier of L;
set ccL = card the carrier of L;
set nccL = nextcard (card the carrier of L);
deffunc H1( Ordinal) -> Element of L = (f,$1) -. a;
consider Ls being Sequence such that
A1:
( dom Ls = nextcard (card the carrier of L) & ( for O2 being Ordinal st O2 in nextcard (card the carrier of L) holds
Ls . O2 = H1(O2) ) )
from ORDINAL2:sch 2();
assume A2:
f . a [= a
; ex O being Ordinal st
( card O c= card the carrier of L & (f,O) -. a is_a_fixpoint_of f )
then consider O being Ordinal such that
A15:
O in nextcard (card the carrier of L)
and
A16:
(f,O) -. a is_a_fixpoint_of f
;
take
O
; ( card O c= card the carrier of L & (f,O) -. a is_a_fixpoint_of f )
card O in nextcard (card the carrier of L)
by A15, CARD_1:9;
hence
card O c= card the carrier of L
by CARD_3:91; (f,O) -. a is_a_fixpoint_of f
thus
(f,O) -. a is_a_fixpoint_of f
by A16; verum