for A being QC-alphabet
for p being Element of CQC-WFF A
for x being Element of bound_QC-variables A holds p is_subformula_of All (x,p)