let a be Ordinal; :: thesis: a c= epsilon_ a
defpred S₁[ Ordinal] means $1 c= epsilon_ $1;
A1: S₁[ 0 ] ;
A2: for b being Ordinal st S₁[b] holds
S₁[ succ b]

proof

let b be Ordinal; :: 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 st c <> 0 & c is limit_ordinal & ( for b being Ordinal st b in c holds
S₁[b] ) holds
S₁[c]

proof

let c be Ordinal; :: thesis: ( c <> 0 & c is limit_ordinal & ( for b being Ordinal st b in c holds
S₁[b] ) implies S₁[c] )
assume that
( c <> 0 & c is limit_ordinal ) and
A5: for b being Ordinal st b in c holds
S₁[b] ; :: thesis: S₁[c]
let x be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not x in c or x in epsilon_ c )
assume A6: x in c ; :: thesis: x in epsilon_ c
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 holds S₁[b] from ORDINAL2:sch 1(A1, A2, A4);
hence a c= epsilon_ a ; :: thesis: verum