theorem Th12: :: QC_LANG3:12

for A being QC-alphabet
for x being bound_QC-variable of A
for p being QC-formula of A holds still_not-bound_in (All (x,p)) = (still_not-bound_in p) \ {x}