let a be ordinal number ; :: thesis: ( 1 in a implies a |^|^ omega is limit_ordinal )
assume Z0: 1 in a ; :: thesis: a |^|^ omega is limit_ordinal
deffunc H₁( Ordinal) -> Ordinal = a |^|^ $1;
consider phi being Ordinal-Sequence such that
A1: ( dom phi = omega & ( for b being ordinal number st b in omega holds
phi . b = H₁(b) ) ) from ORDINAL2:sch 3();
phi is increasing

proof

let b be ordinal number ; :: according to ORDINAL2:def 16 :: thesis: for b₁ being set holds
( not b in b₁ or not b₁ in proj1 phi or phi . b in phi . b₁ )
let c be ordinal number ; :: thesis: ( not b in c or not c in proj1 phi or phi . b in phi . c )
assume A3: ( b in c & c in dom phi ) ; :: thesis: phi . b in phi . c
then reconsider b = b, c = c as Element of NAT by A1, ORDINAL1:19;
b < c by A3, NAT_1:45;
then ( phi . b = H₁(b) & H₁(b) in H₁(c) ) by Z0, A1, Th7;
hence phi . b in phi . c by A1; :: thesis: verum

end;

then ( lim phi = sup phi & sup phi is limit_ordinal ) by A1, ORDINAL4:8, ORDINAL4:16;
hence a |^|^ omega is limit_ordinal by A1, Th2; :: thesis: verum