let a be ordinal number ; :: thesis: ( a is epsilon implies ex b being ordinal number st a = epsilon_ b )
defpred S1[ set ] means ex b being ordinal number st $1 = epsilon_ b;
defpred S2[ Ordinal] means for e being epsilon Ordinal st e in epsilon_ $1 holds
S1[e];
A0: S2[ {} ]
proof
let e be epsilon Ordinal; :: thesis: ( e in epsilon_ {} implies S1[e] )
0 in e by ORDINAL3:10;
then first_epsilon_greater_than 0 c= e by FEGT;
then ( e in epsilon_ 0 implies e in e ) by Th20, Th30;
hence ( e in epsilon_ {} implies S1[e] ) ; :: thesis: verum
end;
A1: for c being ordinal number st S2[c] holds
S2[ succ c]
proof
let c be ordinal number ; :: thesis: ( S2[c] implies S2[ succ c] )
assume Z0: S2[c] ; :: thesis: S2[ succ c]
let e be epsilon Ordinal; :: thesis: ( e in epsilon_ (succ c) implies S1[e] )
assume Z1: e in epsilon_ (succ c) ; :: thesis: S1[e]
Z2: epsilon_ (succ c) = (epsilon_ c) |^|^ omega by Th31
.= first_epsilon_greater_than (epsilon_ c) by Th24 ;
per cases ( e in epsilon_ c or e = epsilon_ c or epsilon_ c in e ) by ORDINAL1:24;
end;
end;
A2: for b being ordinal number st b <> {} & b is limit_ordinal & ( for c being ordinal number st c in b holds
S2[c] ) holds
S2[b]
proof
let b be ordinal number ; :: thesis: ( b <> {} & b is limit_ordinal & ( for c being ordinal number st c in b holds
S2[c] ) implies S2[b] )
assume that
Y0: ( b <> {} & b is limit_ordinal ) and
Y1: for c being ordinal number st c in b holds
S2[c] ; :: thesis: S2[b]
let e be epsilon Ordinal; :: thesis: ( e in epsilon_ b implies S1[e] )
assume e in epsilon_ b ; :: thesis: S1[e]
then ex c being ordinal number st
( c in b & e in epsilon_ c ) by Y0, Th38;
hence S1[e] by Y1; :: thesis: verum
end;
AA: for b being ordinal number holds S2[b] from ORDINAL2:sch 1(A0, A1, A2);
 ( a c= epsilon_ a & epsilon_ a in epsilon_ (succ a) ) by Th33, Th39, ORDINAL1:10;
hence ( a is epsilon implies ex b being ordinal number st a = epsilon_ b ) by AA, ORDINAL1:22; :: thesis: verum