theorem :: QC_LANG3:51

for A being QC-alphabet
for p being Element of QC-WFF A
for V being non empty Subset of (QC-variables A) st p is existential holds
Vars (p,V) = Vars ((the_argument_of (the_scope_of (the_argument_of p))),V)