:: deftheorem Def8 defines the_arity_of QC_LANG1:def 8 :
for A being QC-alphabet
for P being Element of QC-pred_symbols A
for b₃ being Nat holds
( b₃ = the_arity_of P iff P `1 = 7 + b₃ );