let a, b be Ordinal; :: thesis: ( a in b implies epsilon_ a in epsilon_ b )
defpred S₁[ Ordinal] means ( 1 in epsilon_ $1 & ( for a, b being Ordinal st a in b & b c= $1 holds
epsilon_ a in epsilon_ b ) );
omega in epsilon_ 0 by Th26, Th41;
then A1: S₁[ 0 ] by ORDINAL1:10;
A2: for c being Ordinal st S₁[c] holds
S₁[ succ c]

proof

let c be Ordinal; :: thesis: ( S₁[c] implies S₁[ succ c] )
assume A3: S₁[c] ; :: thesis: S₁[ succ c]
A4: epsilon_ (succ c) = (epsilon_ c) |^|^ omega by Th42;
then A5: epsilon_ c in epsilon_ (succ c) by A3, Th26;
hence 1 in epsilon_ (succ c) by A3, ORDINAL1:10; :: thesis: for a, b being Ordinal st a in b & b c= succ c holds
epsilon_ a in epsilon_ b
let a, b be Ordinal; :: thesis: ( a in b & b c= succ c implies epsilon_ a in epsilon_ b )
assume A6: ( a in b & b c= succ c ) ; :: thesis: epsilon_ a in epsilon_ b
then a c= c by ORDINAL1:22;
then A7: ( ( b = succ c & ( a = c or a c< c ) ) or b c< succ c ) by A6;

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

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

then b c= c by ORDINAL1:22;
hence epsilon_ a in epsilon_ b by A3, A6; :: thesis: verum

end;

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

then epsilon_ a in epsilon_ c by A3;
hence epsilon_ a in epsilon_ b by A5, A8, ORDINAL1:10; :: thesis: verum

end;

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

hence epsilon_ a in epsilon_ b by A3, A4, Th26; :: thesis: verum

end;

end;

end;

A9: 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
A10: ( c <> 0 & c is limit_ordinal ) and
A11: for b being Ordinal st b in c holds
S₁[b] ; :: thesis: S₁[c]
deffunc H₁( Ordinal) -> Ordinal = epsilon_ $1;
consider f being Ordinal-Sequence such that
A12: ( dom f = c & ( for b being Ordinal st b in c holds
f . b = H₁(b) ) ) from ORDINAL2:sch 3();
f is increasing

proof

let a be Ordinal; :: according to ORDINAL2:def 12 :: thesis: for b₁ being set holds
( not a in b₁ or not b₁ in dom f or f . a in f . b₁ )
let b be Ordinal; :: thesis: ( not a in b or not b in dom f or f . a in f . b )
assume A13: ( a in b & b in dom f ) ; :: thesis: f . a in f . b
then a in c by A12, ORDINAL1:10;
then ( f . a = H₁(a) & f . b = H₁(b) & S₁[b] ) by A11, A12, A13;
hence f . a in f . b by A13; :: thesis: verum

end;

then Union f is_limes_of f by A10, A12, Th6;
then A14: Union f = lim f by ORDINAL2:def 10
.= epsilon_ c by A10, A12, Th43 ;
A15: 0 in c by A10, ORDINAL3:8;
then ( 1 in epsilon_ 0 & f . 0 = H₁( 0 ) ) by A11, A12;
hence 1 in epsilon_ c by A12, A14, A15, CARD_5:2; :: thesis: for a, b being Ordinal st a in b & b c= c holds
epsilon_ a in epsilon_ b
let a, b be Ordinal; :: thesis: ( a in b & b c= c implies epsilon_ a in epsilon_ b )
assume A16: ( a in b & b c= c ) ; :: thesis: epsilon_ a in epsilon_ b
then A17: ( b = c or b c< c ) ;

per cases ( b in c or b = c ) by A17, ORDINAL1:11;

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

hence epsilon_ a in epsilon_ b by A11, A16; :: thesis: verum

end;

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

( succ a in c & a in succ a ) by A10, A16, ORDINAL1:6, ORDINAL1:28;
then A19: ( H₁(a) in H₁( succ a) & H₁( succ a) = f . (succ a) & f . (succ a) in rng f ) by A11, A12, FUNCT_1:def 3;
then f . (succ a) c= Union f by ZFMISC_1:74;
hence epsilon_ a in epsilon_ b by A14, A18, A19; :: thesis: verum

end;

end;

end;

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