theorem Th2: :: ZF_FUND2:2

for W being Universe
for L being DOMAIN-Sequence of W st ( for a, b being Ordinal of W st a in b holds
L . a c= L . b ) & ( for a being Ordinal of W holds
( L . a in Union L & L . a is epsilon-transitive ) ) & Union L is predicatively_closed holds
Union L |= the_axiom_of_power_sets