:: deftheorem Def12 defines ConsecutiveSet LATTICE5:def 12 :
for A being non empty set
for O being Ordinal
for b₃ being set holds
( b₃ = ConsecutiveSet (A,O) iff ex L0 being Sequence st
( b₃ = last L0 & dom L0 = succ O & L0 . 0 = A & ( for C being Ordinal st succ C in succ O holds
L0 . (succ C) = new_set (L0 . C) ) & ( for C being Ordinal st C in succ O & C <> 0 & C is limit_ordinal holds
L0 . C = union (rng (L0 | C)) ) ) );