:: deftheorem Def18 defines atomic QC_LANG1:def 18 :
for A being QC-alphabet
for F being Element of QC-WFF A holds
( F is atomic iff ex k being Nat ex p being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A st F = p ! ll );