for A being QC-alphabet
for x being bound_QC-variable of A
for p being QC-formula of A st p is closed holds
Ex (x,p) is closed