theorem :: CQC_SIM1:27
for A being QC-alphabet
for p being Element of CQC-WFF A st p is atomic holds
SepVar p = p