theorem Th44: :: QC_LANG3:44

for A being QC-alphabet
for x being bound_QC-variable of A
for p being Element of QC-WFF A
for V being non empty Subset of (QC-variables A) holds Vars ((All (x,p)),V) = Vars (p,V)