let p be Element of CQC-WFF ; :: thesis: ( p is atomic implies SepVar p = p )
assume p is atomic ; :: thesis: SepVar p = p
then ex k being Element of NAT ex P being QC-pred_symbol of k ex ll being CQC-variable_list of st p = P ! ll by Th5;
hence SepVar p = p by Th27; :: thesis: verum