theorem Th6: :: QC_LANG3:6

for A being QC-alphabet
for p being QC-formula of A st p is negative holds
still_not-bound_in p = still_not-bound_in (the_argument_of p)