theorem Th9: :: QC_LANG3:9

for A being QC-alphabet
for p being QC-formula of A st p is conjunctive holds
still_not-bound_in p = (still_not-bound_in (the_left_argument_of p)) \/ (still_not-bound_in (the_right_argument_of p))