:: deftheorem defines QC-pred_symbols QC_LANG1:def 7 :
for A being QC-alphabet holds QC-pred_symbols A = { [n,x] where n is Nat, x is QC-symbol of A : 7 <= n } ;