theorem Th19: :: QC_LANG3:19

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 (Ex (x,p)) = (still_not-bound_in p) \ {x}