let L be complete Lattice; :: thesis: for f being monotone UnOp of L
for b, a 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 b, a being Element of L st b [= a & b is_a_fixpoint_of f holds
for O2 being Ordinal holds b [= (f,O2) -. a
let b, a 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₁[ Ordinal] means b [= (f,$1) -. a;
A3: f . b = b by A2, ABIAN:def 3;

A4: now

let O1 be Ordinal; :: thesis: ( S₁[O1] implies S₁[ succ O1] )
assume S₁[O1] ; :: thesis: S₁[ succ O1]
then f . b [= f . ((f,O1) -. a) by QUANTAL1:def 12;
hence S₁[ succ O1] by A3, Th19; :: thesis: verum

end;

A5: now

deffunc H₁( Ordinal) -> Element of L = (f,$1) -. a;
let O1 be Ordinal; :: thesis: ( O1 <> {} & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S₁[O2] ) implies S₁[O1] )
assume that
A6: ( O1 <> {} & O1 is limit_ordinal ) and
A7: for O2 being Ordinal st O2 in O1 holds
S₁[O2] ; :: thesis: S₁[O1]
consider L1 being T-Sequence such that
A8: ( dom L1 = O1 & ( for O3 being Ordinal st O3 in O1 holds
L1 . O3 = H₁(O3) ) ) from ORDINAL2:sch 2();
A9: b is_less_than rng L1

proof

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 set 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;

(f,O1) -. a = "/\" ((rng L1),L) by A6, A8, Th21;
hence S₁[O1] by A9, LATTICE3:39; :: thesis: verum

end;

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