theorem Th5: :: CQC_SIM1:5

for A being QC-alphabet
for p being Element of CQC-WFF A st p is atomic holds
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