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