theorem Th17: :: QC_LANG3:17

for A being QC-alphabet
for p being QC-formula of A st p is biconditional holds
still_not-bound_in p = (still_not-bound_in (the_left_side_of p)) \/ (still_not-bound_in (the_right_side_of p))