theorem :: ORDINAL1:34

for X being set st ( for a being object st a in X holds
a is Sequence ) & X is c=-linear holds
union X is Sequence