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 Th23, Th41;
then A1: S₁[ 0 ] ;
A2: 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 A3: S₁[b] ; :: thesis: S₁[ succ b]
epsilon_ b in epsilon_ (succ b) by Th44, ORDINAL1:6;
then b in epsilon_ (succ b) by A3, ORDINAL1:12;
hence S₁[ succ b] by ORDINAL1:21; :: thesis: verum

end;

A4: 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
A5: 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 A6: x in c ; :: thesis: x in epsilon_ c
then reconsider a = x as Ordinal ;
( S₁[a] & epsilon_ a in epsilon_ c ) by A5, A6, Th44;
hence x in epsilon_ c by ORDINAL1:12; :: thesis: verum

end;

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