theorem :: SUBSTUT2:26

for Al being QC-alphabet
for p being Element of CQC-WFF Al st p is atomic holds
ex k being Nat ex P being QC-pred_symbol of k,Al ex ll being CQC-variable_list of k,Al st p = P ! ll