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

A4: now

let O1 be Ordinal; :: thesis: ( S₁[O1] implies S₁[ succ O1] )
assume S₁[O1] ; :: thesis: S₁[ succ O1]
then f . (f,O1 +. a) [= f . b by QUANTAL1:def 12;
hence S₁[ succ O1] by A2, Th18; :: 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, Th20;
rng L1 is_less_than b

proof

let q be Element of L; :: according to LATTICE3:def 17 :: thesis: ( not q in rng L1 or q [= b )
assume q in rng L1 ; :: thesis: q [= b
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;
f,O3 +. a [= b by A6, A7, A9;
hence q [= b by A7, A9; :: thesis: verum

end;

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

end;

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