theorem Th7: :: QC_LANG3:7

for A being QC-alphabet
for p being QC-formula of A holds still_not-bound_in ('not' p) = still_not-bound_in p