theorem Th10: :: QC_LANG3:10

for A being QC-alphabet
for p, q being QC-formula of A holds still_not-bound_in (p '&' q) = (still_not-bound_in p) \/ (still_not-bound_in q)