theorem :: QC_LANG2:40

for A being QC-alphabet
for H being Element of QC-WFF A st H is existential holds
H = Ex ((bound_in (the_argument_of H)),(the_argument_of (the_scope_of (the_argument_of H))))