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

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 A2, Th19; :: thesis: verum

end;

A5: now

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 A6: ( O1 <> {} & O1 is limit_ordinal & ( for O2 being Ordinal st O2 in O1 holds
S₁[O2] ) ) ; :: thesis: S₁[O1]
deffunc H₁( Ordinal) -> Element of L = f,$1 -. a;
consider L1 being T-Sequence such that
A7: ( dom L1 = O1 & ( for O3 being Ordinal st O3 in O1 holds
L1 . O3 = H₁(O3) ) ) from ORDINAL2:sch 2();
A8: f,O1 -. a = "/\" (rng L1),L by A6, A7, Th21;
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
A9: ( O3 in dom L1 & q = L1 . O3 ) by FUNCT_1:def 5;
reconsider O3 = O3 as Ordinal by A9;
b [= f,O3 -. a by A6, A7, A9;
hence b [= q by A7, A9; :: thesis: verum

end;

hence S₁[O1] by A8, LATTICE3:40; :: thesis: verum

end;

thus for O2 being Ordinal holds S₁[O2] from ORDINAL2:sch 1(A3, A4, A5); :: thesis: verum