theorem Th18: :: KNASTER:18

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 T being Sequence st O <> 0 & O is limit_ordinal & dom T = O & ( for A being Ordinal st A in O holds
T . A = (f,A) -. x ) holds
(f,O) -. x = "/\" ((rng T),L)