theorem Th16: :: LATTICE8:16

for A being non empty set
for O being Ordinal
for T being Sequence st O <> 0 & O is limit_ordinal & dom T = O & ( for O1 being Ordinal st O1 in O holds
T . O1 = ConsecutiveSet2 (A,O1) ) holds
ConsecutiveSet2 (A,O) = union (rng T)