theorem Th5: :: ZF_FUND2:5

for W being Universe
for Y being Subclass of W st Y is closed_wrt_A1-A7 & Y is epsilon-transitive holds
Y is predicatively_closed