let b be ordinal number ; :: thesis: for x being set st not b is empty & b is limit_ordinal holds
( x in epsilon_ b iff ex c being ordinal number st
( c in b & x in epsilon_ c ) )
let x be set ; :: thesis: ( not b is empty & b is limit_ordinal implies ( x in epsilon_ b iff ex c being ordinal number st
( c in b & x in epsilon_ c ) ) )
assume Z0: ( not b is empty & b is limit_ordinal ) ; :: thesis: ( x in epsilon_ b iff ex c being ordinal number st
( c in b & x in epsilon_ c ) )
deffunc H₁( Ordinal) -> Ordinal = epsilon_ $1;
consider f being Ordinal-Sequence such that
Z1: ( dom f = b & ( for c being ordinal number st c in b holds
f . c = H₁(c) ) ) from ORDINAL2:sch 3();
Z2: Union f = epsilon_ b by Z0, Z1, Th35;

hereby :: thesis: ( ex c being ordinal number st
( c in b & x in epsilon_ c ) implies x in epsilon_ b )

assume x in epsilon_ b ; :: thesis: ex c being Ordinal st
( c in b & x in epsilon_ c )
then consider c being set such that
Z4: ( c in dom f & x in f . c ) by Z2, CARD_5:10;
reconsider c = c as Ordinal by Z4;
take c = c; :: thesis: ( c in b & x in epsilon_ c )
thus c in b by Z1, Z4; :: thesis: x in epsilon_ c
thus x in epsilon_ c by Z1, Z4; :: thesis: verum

end;

given c being ordinal number such that A1: ( c in b & x in epsilon_ c ) ; :: thesis: x in epsilon_ b
f . c = H₁(c) by Z1, A1;
hence x in epsilon_ b by Z1, Z2, A1, CARD_5:10; :: thesis: verum