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

proof

let b be Ordinal; :: according to ORDINAL2:def 12 :: thesis: for b₁ being set holds
( not b in b₁ or not b₁ in dom phi or phi . b in phi . b₁ )
let c be Ordinal; :: thesis: ( not b in c or not c in dom 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 A2, ORDINAL1:10;
b in Segm c by A3;
then b < c by NAT_1:44;
then ( phi . b = H₁(b) & H₁(b) in H₁(c) ) by A1, A2, Th24;
hence phi . b in phi . c by A2; :: thesis: verum

end;

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