:: deftheorem Def5 defines Ex-the_scope_of GOEDELCP:def 5 :
for Al being QC-alphabet
for p being Element of CQC-WFF Al st p is existential holds
for b₃ being Element of CQC-WFF Al holds
( b₃ = Ex-the_scope_of p iff ex x being bound_QC-variable of Al st p = Ex (x,b₃) );