:: deftheorem Def6 defines -closed POLNOT_2:def 6 :
for T being Polish-language
for A being Polish-arity-function of T
for P being non empty FinSequence-membered set holds
( P is A -closed iff for p being FinSequence
for n being Nat
for q being FinSequence st p in T & n = A . p & q in P ^^ n holds
p ^ q in P );