:: deftheorem Def4 defines Ex-bound_in GOEDELCP:def 4 :
for Al being QC-alphabet
for p being Element of QC-WFF Al st p is existential holds
for b₃ being bound_QC-variable of Al holds
( b₃ = Ex-bound_in p iff ex q being Element of QC-WFF Al st p = Ex (b₃,q) );