let A be QC-alphabet ; :: thesis: for p being Element of CQC-WFF A st p is atomic holds
SepVar p = p
let p be Element of CQC-WFF A; :: thesis: ( p is atomic implies SepVar p = p )
assume p is atomic ; :: thesis: SepVar p = p
then ex k being Nat ex P being QC-pred_symbol of k,A ex ll being CQC-variable_list of k,A st p = P ! ll by Th5;
hence SepVar p = p by Th26; :: thesis: verum