for A being QC-alphabet
for p being Element of CQC-WFF A
for x being bound_QC-variable of A holds Ex (x,(p <=> p)) is valid by Lm13, Th16;