theorem Th16: :: ORDINAL4:16

for phi being Ordinal-Sequence st phi is increasing & dom phi is limit_ordinal holds
sup phi is limit_ordinal