:: deftheorem Def22 defines the_pred_symbol_of QC_LANG1:def 22 :
for A being QC-alphabet
for F being Element of QC-WFF A st F is atomic holds
for b₃ being QC-pred_symbol of A holds
( b₃ = the_pred_symbol_of F iff ex k being Nat ex ll being QC-variable_list of k,A ex P being QC-pred_symbol of k,A st
( b₃ = P & F = P ! ll ) );