theorem Th44: :: CQC_SIM1:44
for A being QC-alphabet
for p being Element of CQC-WFF A holds still_not-bound_in p = still_not-bound_in (SepVar p)