:: deftheorem Def10 defines -closed QC_LANG1:def 10 :
for A being QC-alphabet
for D being set holds
( D is A -closed iff ( D is Subset of ([:NAT,(QC-symbols A):] *) & ( for k being Nat
for p being QC-pred_symbol of k,A
for ll being QC-variable_list of k,A holds <*p*> ^ ll in D ) & <*[0,0]*> in D & ( for p being FinSequence of [:NAT,(QC-symbols A):] st p in D holds
<*[1,0]*> ^ p in D ) & ( for p, q being FinSequence of [:NAT,(QC-symbols A):] st p in D & q in D holds
(<*[2,0]*> ^ p) ^ q in D ) & ( for x being bound_QC-variable of A
for p being FinSequence of [:NAT,(QC-symbols A):] st p in D holds
(<*[3,0]*> ^ <*x*>) ^ p in D ) ) );