theorem Th15: :: QC_LANG3:15

for A being QC-alphabet
for p being QC-formula of A st p is conditional holds
still_not-bound_in p = (still_not-bound_in (the_antecedent_of p)) \/ (still_not-bound_in (the_consequent_of p))