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

for a, b being Element of L st b [= a & b is_a_fixpoint_of f holds

for O2 being Ordinal holds b [= (f,O2) -. a

let f be monotone UnOp of L; :: thesis: for a, b being Element of L st b [= a & b is_a_fixpoint_of f holds

for O2 being Ordinal holds b [= (f,O2) -. a

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

assume that

A1: b [= a and

A2: b is_a_fixpoint_of f ; :: thesis: for O2 being Ordinal holds b [= (f,O2) -. a

defpred S_{1}[ Ordinal] means b [= (f,$1) -. a;

A3: f . b = b by A2;

_{1}[ 0 ]
by A1, Th14;

thus for O2 being Ordinal holds S_{1}[O2]
from ORDINAL2:sch 1(A12, A4, A5); :: thesis: verum

for a, b being Element of L st b [= a & b is_a_fixpoint_of f holds

for O2 being Ordinal holds b [= (f,O2) -. a

let f be monotone UnOp of L; :: thesis: for a, b being Element of L st b [= a & b is_a_fixpoint_of f holds

for O2 being Ordinal holds b [= (f,O2) -. a

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

assume that

A1: b [= a and

A2: b is_a_fixpoint_of f ; :: thesis: for O2 being Ordinal holds b [= (f,O2) -. a

defpred S

A3: f . b = b by A2;

A4: now :: thesis: for O1 being Ordinal st S_{1}[O1] holds

S_{1}[ succ O1]

S

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

assume S_{1}[O1]
; :: thesis: S_{1}[ succ O1]

then f . b [= f . ((f,O1) -. a) by QUANTAL1:def 12;

hence S_{1}[ succ O1]
by A3, Th16; :: thesis: verum

end;assume S

then f . b [= f . ((f,O1) -. a) by QUANTAL1:def 12;

hence S

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

S_{1}[O2] ) holds

S_{1}[O1]

A12:
SS

S

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

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

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

assume that

A6: ( O1 <> 0 & O1 is limit_ordinal ) and

A7: for O2 being Ordinal st O2 in O1 holds

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

consider L1 being Sequence such that

A8: ( dom L1 = O1 & ( for O3 being Ordinal st O3 in O1 holds

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

A9: b is_less_than rng L1

hence S_{1}[O1]
by A9, LATTICE3:39; :: thesis: verum

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

S

assume that

A6: ( O1 <> 0 & O1 is limit_ordinal ) and

A7: for O2 being Ordinal st O2 in O1 holds

S

consider L1 being Sequence such that

A8: ( dom L1 = O1 & ( for O3 being Ordinal st O3 in O1 holds

L1 . O3 = H

A9: b is_less_than rng L1

proof

(f,O1) -. a = "/\" ((rng L1),L)
by A6, A8, Th18;
let q be Element of L; :: according to LATTICE3:def 16 :: thesis: ( not q in rng L1 or b [= q )

assume q in rng L1 ; :: thesis: b [= q

then consider O3 being object such that

A10: O3 in dom L1 and

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

reconsider O3 = O3 as Ordinal by A10;

b [= (f,O3) -. a by A7, A8, A10;

hence b [= q by A8, A10, A11; :: thesis: verum

end;assume q in rng L1 ; :: thesis: b [= q

then consider O3 being object such that

A10: O3 in dom L1 and

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

reconsider O3 = O3 as Ordinal by A10;

b [= (f,O3) -. a by A7, A8, A10;

hence b [= q by A8, A10, A11; :: thesis: verum

hence S

thus for O2 being Ordinal holds S