let a be Ordinal; :: thesis: a c= epsilon_ a
defpred S1[ Ordinal] means $1 c= epsilon_ $1;
A1: S1[ 0 ] ;
A2: for b being Ordinal st S1[b] holds
S1[ succ b]
proof
let b be Ordinal; :: thesis: ( S1[b] implies S1[ succ b] )
assume A3: S1[b] ; :: thesis: S1[ succ b]
epsilon_ b in epsilon_ (succ b) by Th44, ORDINAL1:6;
then b in epsilon_ (succ b) by A3, ORDINAL1:12;
hence S1[ 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
S1[b] ) holds
S1[c]
proof
let c be Ordinal; :: thesis: ( c <> 0 & c is limit_ordinal & ( for b being Ordinal st b in c holds
S1[b] ) implies S1[c] )
assume that
( c <> 0 & c is limit_ordinal ) and
A5: for b being Ordinal st b in c holds
S1[b] ; :: thesis: S1[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 ;
( S1[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 S1[b] from ORDINAL2:sch 1(A1, A2, A4);
 hence a c= epsilon_ a ; :: thesis: verum