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