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 :: thesis: for A being Ordinal st A in sup phi holds
succ A in sup phi
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 object such that
A5: x in dom phi and
A6: B = phi . x by ;
reconsider x = x as Ordinal by A5;
A7: succ x in dom phi by ;
reconsider C = phi . (succ x) as Ordinal ;
x in succ x by ORDINAL1:6;
then B in C by A1, A6, A7;
then A8: succ B c= C by ORDINAL1:21;
A9: succ A c= succ B by ;
C in rng phi by ;
then C in sup phi by ORDINAL2:19;
then succ B in sup phi by ;
hence succ A in sup phi by ; :: thesis: verum
end;
hence sup phi is limit_ordinal by ORDINAL1:28; :: thesis: verum