theorem Th3: :: GOEDELCP:3

for Al being QC-alphabet
for X being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al st X is with_examples holds
( X |- Ex (x,p) iff ex y being bound_QC-variable of Al st X |- p . (x,y) )