for A being QC-alphabet
for k being Nat
for P being QC-pred_symbol of k,A
for ll being CQC-variable_list of k,A
for e being Element of vSUB A holds CQC_Sub (Sub_P (P,ll,e)) is Element of CQC-WFF A