deffunc H₁( Ordinal) -> Ordinal = epsilon_ a;
defpred S₁[ Ordinal] means H₁(a) is epsilon ;
A1: S₁[ 0 ] by Th36, Th41;
A2: for b being Ordinal st S₁[b] holds
S₁[ succ b]

end;

A3: for b being Ordinal st b <> 0 & b is limit_ordinal & ( for c being Ordinal st c in b holds
S₁[c] ) holds
S₁[b]

let b be Ordinal; :: thesis:
assume that
A4: ( b <> 0 & b is limit_ordinal ) and
A5: for c being Ordinal st c in b holds
S₁[c] ; :: thesis:
consider f being Ordinal-Sequence such that
A6: ( dom f = b & ( for c being Ordinal st c in b holds
f . c = H₁(c) ) ) from ORDINAL2:sch 3();
A7: H₁(b) = Union f by A4, A6, Th46;
set X = rng f;
0 in b by A4, ORDINAL3:8;
then f . 0 in rng f by A6, FUNCT_1:def 3;
then reconsider X = rng f as non empty set ;

let x be object ; :: thesis:
assume x in X ; :: thesis:
then consider a being object such that
A9: ( a in dom f & f . a = x ) by FUNCT_1:def 3;
reconsider a = a as Ordinal by A9;
x = H₁(a) by A6, A9;
hence x is epsilon Ordinal by A5, A6, A9; :: thesis:

end;

let x be Ordinal; :: thesis:
assume A10: x in X ; :: thesis:
then consider a being object such that
A11: ( a in dom f & f . a = x ) by FUNCT_1:def 3;
reconsider a = a as Ordinal by A11;
A12: succ a in b by A4, A6, A11, ORDINAL1:28;
reconsider e = x as epsilon Ordinal by A8, A10;
e = H₁(a) by A6, A11;
then first_epsilon_greater_than e = H₁(a) |^|^ omega by Th40
.= H₁( succ a) by Th42
.= f . (succ a) by A6, A12 ;
hence first_epsilon_greater_than x in X by A6, A12, FUNCT_1:def 3; :: thesis:

end;

end;