theorem :: QC_LANG3:18

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