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