theorem :: CQC_THE2:11

for A being QC-alphabet
for s being QC-formula of A
for x, y being bound_QC-variable of A holds
( not x in still_not-bound_in (Ex (x,y,s)) & not y in still_not-bound_in (Ex (x,y,s)) )