theorem :: CQC_THE2:58

for A being QC-alphabet
for p, q being Element of CQC-WFF A
for h being QC-formula of A
for x, y being bound_QC-variable of A st p = h . x & q = h . y & not y in still_not-bound_in h holds
(Ex (x,p)) => (Ex (x,y,q)) is valid