let a be Ordinal; :: thesis: ( a is epsilon implies ex b being Ordinal st a = epsilon_ b )
defpred S1[ set ] means ex b being Ordinal st $1 = epsilon_ b;
defpred S2[ Ordinal] means for e being epsilon Ordinal st e in epsilon_ $1 holds
S1[e];
A1: S2[ 0 ]
proof
let e be epsilon Ordinal; :: thesis: ( e in epsilon_ 0 implies S1[e] )
0 in e by ORDINAL3:8;
then first_epsilon_greater_than 0 c= e by Def6;
then ( e in epsilon_ 0 implies e in e ) by Th36, Th41;
hence ( e in epsilon_ 0 implies S1[e] ) ; :: thesis: verum
end;
A2: for c being Ordinal st S2[c] holds
S2[ succ c]
proof
let c be Ordinal; :: thesis: ( S2[c] implies S2[ succ c] )
assume A3: S2[c] ; :: thesis: S2[ succ c]
let e be epsilon Ordinal; :: thesis: ( e in epsilon_ (succ c) implies S1[e] )
assume A4: e in epsilon_ (succ c) ; :: thesis: S1[e]
A5: epsilon_ (succ c) = (epsilon_ c) |^|^ omega by Th42
.= first_epsilon_greater_than (epsilon_ c) by Th40 ;
per cases ( e in epsilon_ c or e = epsilon_ c or epsilon_ c in e ) by ORDINAL1:14;
end;
end;
A6: for b being Ordinal st b <> 0 & b is limit_ordinal & ( for c being Ordinal st c in b holds
S2[c] ) holds
S2[b]
proof
let b be Ordinal; :: thesis: ( b <> 0 & b is limit_ordinal & ( for c being Ordinal st c in b holds
S2[c] ) implies S2[b] )
assume that
A7: ( b <> 0 & b is limit_ordinal ) and
A8: for c being Ordinal 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 st
( c in b & e in epsilon_ c ) by A7, Th47;
hence S1[e] by A8; :: thesis: verum
end;
A9: for b being Ordinal holds S2[b] from ORDINAL2:sch 1(A1, A2, A6);
 ( a c= epsilon_ a & epsilon_ a in epsilon_ (succ a) ) by Th44, Th48, ORDINAL1:6;
hence ( a is epsilon implies ex b being Ordinal st a = epsilon_ b ) by A9, ORDINAL1:12; :: thesis: verum