:: deftheorem Def6 defines bound_in GOEDELCP:def 6 :
for Al being QC-alphabet
for F being sequence of (CQC-WFF Al)
for a being Nat
for b₄ being bound_QC-variable of Al holds
( b₄ = bound_in (F,a) iff for p being Element of CQC-WFF Al st p = F . a holds
b₄ = Ex-bound_in p );