:: deftheorem Def2 defines free_symbol GOEDCPUC:def 2 :
for Al being QC-alphabet
for b₂ being set holds
( b₂ is free_symbol of Al iff for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al holds not [b₂,[x,p]] in QC-symbols Al );