theorem Th22: :: CQC_THE2:22

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
p => (Ex (y,q)) is valid