for A being QC-alphabet
for x being bound_QC-variable of A
for S being Element of QC-Sub-WFF A
for xSQ being second_Q_comp of [S,x] st CQC_Sub S is Element of CQC-WFF A & [S,x] is quantifiable holds
CQC_Sub (Sub_All ([S,x],xSQ)) is Element of CQC-WFF A