let a, b be ordinal number ; :: thesis: ( a in b implies epsilon_ a in epsilon_ b )
defpred S₁[ Ordinal] means ( 1 in epsilon_ $1 & ( for a, b being ordinal number st a in b & b c= $1 holds
epsilon_ a in epsilon_ b ) );
omega in epsilon_ 0 by Th9, Th30;
then A0: S₁[ 0 ] by ORDINAL1:19;
A1: for c being ordinal number st S₁[c] holds
S₁[ succ c]

proof

let c be ordinal number ; :: thesis: ( S₁[c] implies S₁[ succ c] )
assume B1: S₁[c] ; :: thesis: S₁[ succ c]
epsilon_ (succ c) = (epsilon_ c) |^|^ omega by Th31;
then B4: epsilon_ c in epsilon_ (succ c) by B1, Th9;
hence 1 in epsilon_ (succ c) by B1, ORDINAL1:19; :: thesis: for a, b being ordinal number st a in b & b c= succ c holds
epsilon_ a in epsilon_ b
let a, b be ordinal number ; :: thesis: ( a in b & b c= succ c implies epsilon_ a in epsilon_ b )
assume B2: ( a in b & b c= succ c ) ; :: thesis: epsilon_ a in epsilon_ b
then a c= c by ORDINAL1:34;
then B3: ( ( b = succ c & ( a = c or a c< c ) ) or b c< succ c ) by B2, XBOOLE_0:def 8;

per cases ( b in succ c or ( b = succ c & a in c ) or ( b = succ c & a = c ) ) by B3, ORDINAL1:21;

suppose b in succ c ; :: thesis: epsilon_ a in epsilon_ b

then b c= c by ORDINAL1:34;
hence epsilon_ a in epsilon_ b by B1, B2; :: thesis: verum

end;

suppose B5: ( b = succ c & a in c ) ; :: thesis: epsilon_ a in epsilon_ b

then epsilon_ a in epsilon_ c by B1;
hence epsilon_ a in epsilon_ b by B4, B5, ORDINAL1:19; :: thesis: verum

end;

suppose ( b = succ c & a = c ) ; :: thesis: epsilon_ a in epsilon_ b

hence epsilon_ a in epsilon_ b by B4; :: thesis: verum

end;

end;

end;

A2: 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
C1: ( c <> {} & c is limit_ordinal ) and
C2: for b being ordinal number st b in c holds
S₁[b] ; :: thesis: S₁[c]
deffunc H₁( Ordinal) -> Ordinal = epsilon_ $1;
consider f being Ordinal-Sequence such that
C3: ( dom f = c & ( for b being ordinal number st b in c holds
f . b = H₁(b) ) ) from ORDINAL2:sch 3();
f is increasing

proof

let a be ordinal number ; :: according to ORDINAL2:def 16 :: thesis: for b₁ being set holds
( not a in b₁ or not b₁ in proj1 f or f . a in f . b₁ )
let b be ordinal number ; :: thesis: ( not a in b or not b in proj1 f or f . a in f . b )
assume C4: ( a in b & b in dom f ) ; :: thesis: f . a in f . b
then a in c by C3, ORDINAL1:19;
then ( f . a = H₁(a) & f . b = H₁(b) & S₁[b] ) by C2, C3, C4;
hence f . a in f . b by C4; :: thesis: verum

end;

then Union f is_limes_of f by C1, C3, ThND;
then C5: Union f = lim f by ORDINAL2:def 14
.= epsilon_ c by C1, C3, Th32 ;
C6: 0 in c by C1, ORDINAL3:10;
then ( 1 in epsilon_ 0 & f . 0 = H₁( 0 ) ) by C2, C3;
hence 1 in epsilon_ c by C3, C5, C6, CARD_5:10; :: thesis: for a, b being ordinal number st a in b & b c= c holds
epsilon_ a in epsilon_ b
let a, b be ordinal number ; :: thesis: ( a in b & b c= c implies epsilon_ a in epsilon_ b )
assume C7: ( a in b & b c= c ) ; :: thesis: epsilon_ a in epsilon_ b
then C8: ( b = c or b c< c ) by XBOOLE_0:def 8;

per cases ( b in c or b = c ) by C8, ORDINAL1:21;

suppose b in c ; :: thesis: epsilon_ a in epsilon_ b

hence epsilon_ a in epsilon_ b by C2, C7; :: thesis: verum

end;

suppose C9: b = c ; :: thesis: epsilon_ a in epsilon_ b

( succ a in c & a in succ a ) by C1, C7, ORDINAL1:10, ORDINAL1:41;
then D1: ( H₁(a) in H₁( succ a) & H₁( succ a) = f . (succ a) & f . (succ a) in rng f ) by C2, C3, FUNCT_1:def 5;
then f . (succ a) c= Union f by ZFMISC_1:92;
hence epsilon_ a in epsilon_ b by C5, C9, D1; :: thesis: verum

end;

end;

end;

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