let O1 be Ordinal; :: thesis: for L being complete Lattice

for f being monotone UnOp of L

for a being Element of L st a [= f . a & (f,O1) +. a is_a_fixpoint_of f holds

for O2 being Ordinal st O1 c= O2 holds

(f,O1) +. a = (f,O2) +. a

let L be complete Lattice; :: thesis: for f being monotone UnOp of L

for a being Element of L st a [= f . a & (f,O1) +. a is_a_fixpoint_of f holds

for O2 being Ordinal st O1 c= O2 holds

(f,O1) +. a = (f,O2) +. a

let f be monotone UnOp of L; :: thesis: for a being Element of L st a [= f . a & (f,O1) +. a is_a_fixpoint_of f holds

for O2 being Ordinal st O1 c= O2 holds

(f,O1) +. a = (f,O2) +. a

let a be Element of L; :: thesis: ( a [= f . a & (f,O1) +. a is_a_fixpoint_of f implies for O2 being Ordinal st O1 c= O2 holds

(f,O1) +. a = (f,O2) +. a )

assume that

A1: a [= f . a and

A2: (f,O1) +. a is_a_fixpoint_of f ; :: thesis: for O2 being Ordinal st O1 c= O2 holds

(f,O1) +. a = (f,O2) +. a

set fa = (f,O1) +. a;

defpred S_{1}[ Ordinal] means ( O1 c= $1 implies (f,O1) +. a = (f,$1) +. a );

_{1}[ 0 ]
;

thus for O2 being Ordinal holds S_{1}[O2]
from ORDINAL2:sch 1(A14, A11, A3); :: thesis: verum

for f being monotone UnOp of L

for a being Element of L st a [= f . a & (f,O1) +. a is_a_fixpoint_of f holds

for O2 being Ordinal st O1 c= O2 holds

(f,O1) +. a = (f,O2) +. a

let L be complete Lattice; :: thesis: for f being monotone UnOp of L

for a being Element of L st a [= f . a & (f,O1) +. a is_a_fixpoint_of f holds

for O2 being Ordinal st O1 c= O2 holds

(f,O1) +. a = (f,O2) +. a

let f be monotone UnOp of L; :: thesis: for a being Element of L st a [= f . a & (f,O1) +. a is_a_fixpoint_of f holds

for O2 being Ordinal st O1 c= O2 holds

(f,O1) +. a = (f,O2) +. a

let a be Element of L; :: thesis: ( a [= f . a & (f,O1) +. a is_a_fixpoint_of f implies for O2 being Ordinal st O1 c= O2 holds

(f,O1) +. a = (f,O2) +. a )

assume that

A1: a [= f . a and

A2: (f,O1) +. a is_a_fixpoint_of f ; :: thesis: for O2 being Ordinal st O1 c= O2 holds

(f,O1) +. a = (f,O2) +. a

set fa = (f,O1) +. a;

defpred S

A3: now :: thesis: for O2 being Ordinal st O2 <> 0 & O2 is limit_ordinal & ( for O3 being Ordinal st O3 in O2 holds

S_{1}[O3] ) holds

S_{1}[O2]

S

S

let O2 be Ordinal; :: thesis: ( O2 <> 0 & O2 is limit_ordinal & ( for O3 being Ordinal st O3 in O2 holds

S_{1}[O3] ) implies S_{1}[O2] )

assume that

A4: ( O2 <> 0 & O2 is limit_ordinal ) and

A5: for O3 being Ordinal st O3 in O2 holds

S_{1}[O3]
; :: thesis: S_{1}[O2]

thus S_{1}[O2]
:: thesis: verum

end;S

assume that

A4: ( O2 <> 0 & O2 is limit_ordinal ) and

A5: for O3 being Ordinal st O3 in O2 holds

S

thus S

proof

assume
O1 c= O2
; :: thesis: (f,O1) +. a = (f,O2) +. a

then A6: (f,O1) +. a [= (f,O2) +. a by A1, Th24;

deffunc H_{1}( Ordinal) -> Element of L = (f,$1) +. a;

consider L1 being Sequence such that

A7: ( dom L1 = O2 & ( for O3 being Ordinal st O3 in O2 holds

L1 . O3 = H_{1}(O3) ) )
from ORDINAL2:sch 2();

A8: rng L1 is_less_than (f,O1) +. a

then (f,O2) +. a [= (f,O1) +. a by A8, LATTICE3:def 21;

hence (f,O1) +. a = (f,O2) +. a by A6, LATTICES:8; :: thesis: verum

end;then A6: (f,O1) +. a [= (f,O2) +. a by A1, Th24;

deffunc H

consider L1 being Sequence such that

A7: ( dom L1 = O2 & ( for O3 being Ordinal st O3 in O2 holds

L1 . O3 = H

A8: rng L1 is_less_than (f,O1) +. a

proof

(f,O2) +. a = "\/" ((rng L1),L)
by A4, A7, Th17;
let q be Element of L; :: according to LATTICE3:def 17 :: thesis: ( not q in rng L1 or q [= (f,O1) +. a )

assume q in rng L1 ; :: thesis: q [= (f,O1) +. a

then consider O3 being object such that

A9: O3 in dom L1 and

A10: q = L1 . O3 by FUNCT_1:def 3;

reconsider O3 = O3 as Ordinal by A9;

end;assume q in rng L1 ; :: thesis: q [= (f,O1) +. a

then consider O3 being object such that

A9: O3 in dom L1 and

A10: q = L1 . O3 by FUNCT_1:def 3;

reconsider O3 = O3 as Ordinal by A9;

then (f,O2) +. a [= (f,O1) +. a by A8, LATTICE3:def 21;

hence (f,O1) +. a = (f,O2) +. a by A6, LATTICES:8; :: thesis: verum

A11: now :: thesis: for O2 being Ordinal st S_{1}[O2] holds

S_{1}[ succ O2]

A14:
SS

let O2 be Ordinal; :: thesis: ( S_{1}[O2] implies S_{1}[ succ O2] )

assume A12: S_{1}[O2]
; :: thesis: S_{1}[ succ O2]

thus S_{1}[ succ O2]
:: thesis: verum

end;assume A12: S

thus S

thus for O2 being Ordinal holds S