theorem Th13: :: QC_LANG3:13

for A being QC-alphabet
for p being QC-formula of A st p is disjunctive holds
still_not-bound_in p = (still_not-bound_in (the_left_disjunct_of p)) \/ (still_not-bound_in (the_right_disjunct_of p))