theorem Th8: :: ZF_FUND1:8

for V being Universe
for X being Subclass of V
for fs being finite Subset of omega st X is closed_wrt_A1-A7 holds
Funcs (fs,omega) c= X