:: deftheorem defines -closed POLNOT_1:def 15 :
for B being natural-valued Function
for Q being FinSequence-membered set holds
( Q is B -closed iff for p being FinSequence
for n being Nat
for q being FinSequence st p in dom B & n = B . p & q in Q ^^ n holds
p ^ q in Q );