for A being QC-alphabet
for p being Element of CQC-WFF A st p is universal holds
ex x being Element of bound_QC-variables A ex q being Element of CQC-WFF A st p = All (x,q)