let b be Ordinal; :: thesis: for x being object st not b is empty & b is limit_ordinal holds
( x in epsilon_ b iff ex c being Ordinal st
( c in b & x in epsilon_ c ) )
let x be object ; :: thesis: ( not b is empty & b is limit_ordinal implies ( x in epsilon_ b iff ex c being Ordinal st
( c in b & x in epsilon_ c ) ) )
assume A1: ( not b is empty & b is limit_ordinal ) ; :: thesis: ( x in epsilon_ b iff ex c being Ordinal st
( c in b & x in epsilon_ c ) )
deffunc H1( Ordinal) -> Ordinal = epsilon_ $1;
consider f being Ordinal-Sequence such that
A2: ( dom f = b & ( for c being Ordinal st c in b holds
f . c = H1(c) ) ) from ORDINAL2:sch 3();
 A3: Union f = epsilon_ b by A1, A2, Th46;
hereby :: thesis: ( ex c being Ordinal 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 object such that
A4: ( c in dom f & x in f . c ) by A3, CARD_5:2;
reconsider c = c as Ordinal by A4;
take c = c; :: thesis: ( c in b & x in epsilon_ c )
thus c in b by A2, A4; :: thesis: x in epsilon_ c
thus x in epsilon_ c by A2, A4; :: thesis: verum
end;
given c being Ordinal such that A5: ( c in b & x in epsilon_ c ) ; :: thesis: x in epsilon_ b
f . c = H1(c) by A2, A5;
hence x in epsilon_ b by A2, A3, A5, CARD_5:2; :: thesis: verum