for C being Ordinal
for phi being Ordinal-Sequence st phi is increasing holds
C +^ phi is increasing