:: deftheorem defines Sub_atomic SUBSTUT1:def 25 :
for A being QC-alphabet
for S being Element of QC-Sub-WFF A holds
( S is Sub_atomic iff ex k being Nat ex P being QC-pred_symbol of k,A ex ll being QC-variable_list of k,A ex e being Element of vSUB A st S = Sub_P (P,ll,e) );