theorem :: QC_LANG2:28

for A being QC-alphabet
for x, y, z being bound_QC-variable of A
for p being Element of QC-WFF A holds
( Ex (x,y,p) is existential & Ex (x,y,z,p) is existential ) ;