let L be complete Lattice; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 H₁( 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 = H₁(O2) ) ) from ORDINAL2:sch 2();
assume A2: f . a [= a ; :: thesis: ex O being Ordinal st
( card O c= card the carrier of L & (f,O) -. a is_a_fixpoint_of f )

now :: thesis: ex O being Ordinal st
( O in nextcard (card the carrier of L) & (f,O) -. a is_a_fixpoint_of f )

assume A3: for O being Ordinal st O in nextcard (card the carrier of L) holds
not (f,O) -. a is_a_fixpoint_of f ; :: thesis: contradiction
A4: Ls is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in dom Ls or not x2 in dom Ls or not Ls . x1 = Ls . x2 or x1 = x2 )
assume that
A5: x1 in dom Ls and
A6: x2 in dom Ls and
A7: Ls . x1 = Ls . x2 ; :: thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as Ordinal by A5, A6;
A8: Ls . x1 = (f,x1) -. a by A1, A5;
A9: Ls . x2 = (f,x2) -. a by A1, A6;

per cases ( x1 c< x2 or x2 c< x1 or x2 = x1 ) by Lm1;

suppose A10: x1 c< x2 ; :: thesis: x1 = x2

not (f,x2) -. a is_a_fixpoint_of f by A1, A3, A6;
hence x1 = x2 by A2, A1, A6, A7, A8, A10, Th27; :: thesis: verum

end;

suppose A11: x2 c< x1 ; :: thesis: x1 = x2

not (f,x1) -. a is_a_fixpoint_of f by A1, A3, A5;
hence x1 = x2 by A2, A1, A5, A7, A9, A11, Th27; :: thesis: verum

end;

suppose x2 = x1 ; :: thesis: x1 = x2

hence x1 = x2 ; :: thesis: verum

end;

end;

end;

rng Ls c= the carrier of L

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng Ls or y in the carrier of L )
assume y in rng Ls ; :: thesis: y in the carrier of L
then consider x being object such that
A12: x in dom Ls and
A13: Ls . x = y by FUNCT_1:def 3;
reconsider x = x as Ordinal by A12;
Ls . x = (f,x) -. a by A1, A12;
hence y in the carrier of L by A13; :: thesis: verum

end;

then card (nextcard (card the carrier of L)) c= card the carrier of L by A1, A4, CARD_1:10;
then A14: nextcard (card the carrier of L) c= card the carrier of L ;
card the carrier of L in nextcard (card the carrier of L) by CARD_1:18;
hence contradiction by A14, CARD_1:4; :: thesis: verum

end;

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 ; :: thesis: ( 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; :: thesis: (f,O) -. a is_a_fixpoint_of f
thus (f,O) -. a is_a_fixpoint_of f by A16; :: thesis: verum