let phi be Ordinal-Sequence; :: thesis: ( phi is increasing & dom phi is limit_ordinal implies sup phi is limit_ordinal )
assume that
A1: phi is increasing and
A2: dom phi is limit_ordinal ; :: thesis: sup phi is limit_ordinal

now

let A be Ordinal; :: thesis: ( A in sup phi implies succ A in sup phi )
assume A in sup phi ; :: thesis: succ A in sup phi
then consider B being Ordinal such that
A3: B in rng phi and
A4: A c= B by ORDINAL2:21;
consider x being set such that
A5: x in dom phi and
A6: B = phi . x by A3, FUNCT_1:def 3;
reconsider x = x as Ordinal by A5;
A7: succ x in dom phi by A2, A5, ORDINAL1:28;
reconsider C = phi . (succ x) as Ordinal ;
x in succ x by ORDINAL1:6;
then B in C by A1, A6, A7, ORDINAL2:def 12;
then A8: succ B c= C by ORDINAL1:21;
A9: succ A c= succ B by A4, ORDINAL2:1;
C in rng phi by A7, FUNCT_1:def 3;
then C in sup phi by ORDINAL2:19;
then succ B in sup phi by A8, ORDINAL1:12;
hence succ A in sup phi by A9, ORDINAL1:12; :: thesis: verum

end;

hence sup phi is limit_ordinal by ORDINAL1:28; :: thesis: verum