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

A3: now

let O1 be Ordinal; :: thesis: ( S₁[O1] implies S₁[ succ O1] )
assume S₁[O1] ; :: thesis: S₁[ succ O1]
then f . (f,O1 +. (Bottom L)) [= f . a by QUANTAL1:def 12;
hence S₁[ succ O1] by A1, Th18; :: thesis: verum

end;

A4: 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 A5: ( 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 +. (Bottom L);
consider L1 being T-Sequence such that
A6: ( dom L1 = O1 & ( for O3 being Ordinal st O3 in O1 holds
L1 . O3 = H₁(O3) ) ) from ORDINAL2:sch 2();
A7: f,O1 +. (Bottom L) = "\/" (rng L1),L by A5, A6, Th20;
rng L1 is_less_than a

proof

let q be Element of L; :: according to LATTICE3:def 17 :: thesis: ( not q in rng L1 or q [= a )
assume q in rng L1 ; :: thesis: q [= a
then consider C being set such that
A8: ( C in dom L1 & q = L1 . C ) by FUNCT_1:def 5;
reconsider C = C as Ordinal by A8;
f,C +. (Bottom L) [= a by A5, A6, A8;
hence q [= a by A6, A8; :: thesis: verum

end;

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

end;

for O2 being Ordinal holds S₁[O2] from ORDINAL2:sch 1(A2, A3, A4);
hence lfp f [= a ; :: thesis: a [= gfp f
defpred S₂[ Ordinal] means a [= f,$1 -. (Top L);
f,{} -. (Top L) = Top L by Th17;
then A9: S₂[ {} ] by LATTICES:45;

A10: now

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

end;

A11: 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 A12: ( 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 -. (Top L);
consider L1 being T-Sequence such that
A13: ( dom L1 = O1 & ( for O3 being Ordinal st O3 in O1 holds
L1 . O3 = H₁(O3) ) ) from ORDINAL2:sch 2();
A14: f,O1 -. (Top L) = "/\" (rng L1),L by A12, A13, Th21;
a is_less_than rng L1

proof

let q be Element of L; :: according to LATTICE3:def 16 :: thesis: ( not q in rng L1 or a [= q )
assume q in rng L1 ; :: thesis: a [= q
then consider C being set such that
A15: ( C in dom L1 & q = L1 . C ) by FUNCT_1:def 5;
reconsider C = C as Ordinal by A15;
a [= f,C -. (Top L) by A12, A13, A15;
hence a [= q by A13, A15; :: thesis: verum

end;

hence S₂[O1] by A14, LATTICE3:40; :: thesis: verum

end;

for O2 being Ordinal holds S₂[O2] from ORDINAL2:sch 1(A9, A10, A11);
hence a [= gfp f ; :: thesis: verum