theorem Th23: :: LATTICE5:23

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