let a, b be ordinal number ; :: thesis: for x being set st 0 in a & not b is empty & b is limit_ordinal holds
( x in exp a,b iff ex c being ordinal number st
( c in b & x in exp a,c ) )
let x be set ; :: thesis: ( 0 in a & not b is empty & b is limit_ordinal implies ( x in exp a,b iff ex c being ordinal number st
( c in b & x in exp a,c ) ) )
assume Z0: ( 0 in a & not b is empty & b is limit_ordinal ) ; :: thesis: ( x in exp a,b iff ex c being ordinal number st
( c in b & x in exp a,c ) )
deffunc H₁( Ordinal) -> set = exp a,$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();
f is non-decreasing by Z0, Z1, Th003;
then Union f is_limes_of f by Z0, Z1, ThND;
then Z2: Union f = lim f by ORDINAL2:def 14
.= exp a,b by Z0, Z1, ORDINAL2:62 ;

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

assume x in exp a,b ; :: thesis: ex c being Ordinal st
( c in b & x in exp a,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 exp a,c )
thus c in b by Z1, Z4; :: thesis: x in exp a,c
thus x in exp a,c by Z1, Z4; :: thesis: verum

end;

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