:: deftheorem defines -ary_QC-pred_symbols QC_LANG1:def 9 :
for A being QC-alphabet
for k being Nat holds k -ary_QC-pred_symbols A = { P where P is QC-pred_symbol of A : the_arity_of P = k } ;