let phi be Ordinal-Sequence; :: thesis: ( phi is increasing & dom phi is limit_ordinal implies sup phi is limit_ordinal )
assume A1: ( phi is increasing & 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
A2: ( B in rng phi & A c= B ) by ORDINAL2:29;
consider x being set such that
A3: ( x in dom phi & B = phi . x ) by A2, FUNCT_1:def 5;
reconsider x = x as Ordinal by A3;
A4: ( x in succ x & succ x in dom phi ) by A1, A3, ORDINAL1:10, ORDINAL1:41;
reconsider C = phi . (succ x) as Ordinal ;
( B in C & C in rng phi ) by A1, A3, A4, FUNCT_1:def 5, ORDINAL2:def 16;
then ( succ B c= C & C in sup phi ) by ORDINAL1:33, ORDINAL2:27;
then ( succ A c= succ B & succ B in sup phi ) by A2, ORDINAL1:22, ORDINAL2:1;
hence succ A in sup phi by ORDINAL1:22; :: thesis: verum

end;

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