theorem Th15: :: ZF_FUND1:15

for V being Universe
for a, y being Element of V
for X being Subclass of V
for fs being finite Subset of omega
for n being Element of omega st X is closed_wrt_A1-A7 & a in X & a c= X & y in Funcs (fs,a) holds
{ ({[n,x]} \/ y) where x is Element of V : x in a } in X