theorem Th16: :: QC_LANG3:16

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)