:: deftheorem Def5 defines -. KNASTER:def 5 :
for L being Lattice
for f being Function of the carrier of L, the carrier of L
for x being Element of L
for O being Ordinal
for b₅ being set holds
( b₅ = (f,O) -. x iff ex L0 being Sequence st
( b₅ = last L0 & dom L0 = succ O & L0 . 0 = x & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = f . (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> 0 & C is limit_ordinal holds
L0 . C = "/\" ((rng (L0 | C)),L) ) ) );