let L be complete Lattice; :: thesis: for f being monotone UnOp of L
for a being Element of L st a [= f . 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 a [= f . 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: ( a [= f . a implies ex O being Ordinal st
( card O c= card the carrier of L & f,O +. a is_a_fixpoint_of f ) )
assume A1: a [= f . a ; :: thesis: 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 T-Sequence such that
A2: ( 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();

now

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 set ; :: according to FUNCT_1:def 8 :: thesis: ( not x1 in dom Ls or not x2 in dom Ls or not Ls . x1 = Ls . x2 or x1 = x2 )
assume A5: ( x1 in dom Ls & x2 in dom Ls & Ls . x1 = Ls . x2 ) ; :: thesis: x1 = x2
then reconsider x1 = x1, x2 = x2 as Ordinal ;
A6: ( Ls . x1 = f,x1 +. a & Ls . x2 = f,x2 +. a ) by A2, A5;

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

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

not f,x2 +. a is_a_fixpoint_of f by A2, A3, A5;
hence x1 = x2 by A1, A5, A6, A7, Th29; :: thesis: verum

end;

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

not f,x1 +. a is_a_fixpoint_of f by A2, A3, A5;
hence x1 = x2 by A1, A5, A6, A8, Th29; :: 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 set ; :: 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 set such that
A9: ( x in dom Ls & Ls . x = y ) by FUNCT_1:def 5;
reconsider x = x as Ordinal by A9;
Ls . x = f,x +. a by A2, A9;
hence y in the carrier of L by A9; :: thesis: verum

end;

then card (nextcard (card the carrier of L)) c= card the carrier of L by A2, A4, CARD_1:26;
then ( 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:32, CARD_1:def 5;
hence contradiction by CARD_1:14; :: thesis: verum

end;

then consider O being Ordinal such that
A10: ( O in nextcard (card the carrier of L) & 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 A10, CARD_1:25;
hence card O c= card the carrier of L by CARD_3:108; :: thesis: f,O +. a is_a_fixpoint_of f
thus f,O +. a is_a_fixpoint_of f by A10; :: thesis: verum