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:29;
consider x being set such that
A5: x in dom phi and
A6: B = phi . x by A3, FUNCT_1:def 5;
reconsider x = x as Ordinal by A5;
A7: succ x in dom phi by A2, A5, ORDINAL1:41;
reconsider C = phi . (succ x) as Ordinal ;
x in succ x by ORDINAL1:10;
then B in C by A1, A6, A7, ORDINAL2:def 16;
then A8: succ B c= C by ORDINAL1:33;
A9: succ A c= succ B by A4, ORDINAL2:1;
C in rng phi by A7, FUNCT_1:def 5;
then C in sup phi by ORDINAL2:27;
then succ B in sup phi by A8, ORDINAL1:22;
hence succ A in sup phi by A9, ORDINAL1:22; :: thesis: verum

end;

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