let a be ordinal number ; :: thesis: a c= epsilon_ a
defpred S₁[ Ordinal] means $1 c= epsilon_ $1;
( 0 in omega & omega c= epsilon_ 0 ) by Th6, Th30;
then A0: S₁[ 0 ] ;
A1: for b being ordinal number st S₁[b] holds
S₁[ succ b]

proof

let b be ordinal number ; :: thesis: ( S₁[b] implies S₁[ succ b] )
assume Z0: S₁[b] ; :: thesis: S₁[ succ b]
epsilon_ b in epsilon_ (succ b) by Th33, ORDINAL1:10;
then b in epsilon_ (succ b) by Z0, ORDINAL1:22;
hence S₁[ succ b] by ORDINAL1:33; :: thesis: verum

end;

A2: for c being ordinal number st c <> {} & c is limit_ordinal & ( for b being ordinal number st b in c holds
S₁[b] ) holds
S₁[c]

proof

let c be ordinal number ; :: thesis: ( c <> {} & c is limit_ordinal & ( for b being ordinal number st b in c holds
S₁[b] ) implies S₁[c] )
assume that
( c <> {} & c is limit_ordinal ) and
Z1: for b being ordinal number st b in c holds
S₁[b] ; :: thesis: S₁[c]
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in c or x in epsilon_ c )
assume Z2: x in c ; :: thesis: x in epsilon_ c
then reconsider a = x as Ordinal ;
( S₁[a] & epsilon_ a in epsilon_ c ) by Z1, Z2, Th33;
hence x in epsilon_ c by ORDINAL1:22; :: thesis: verum

end;

for b being ordinal number holds S₁[b] from ORDINAL2:sch 1(A0, A1, A2);
hence a c= epsilon_ a ; :: thesis: verum