theorem Th10: :: GOEDELCP:10

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for CX being Consistent Subset of (CQC-WFF Al)
for JH being Henkin_interpretation of CX holds
( JH, valH Al |= Ex (x,p) iff ex y being bound_QC-variable of Al st JH, valH Al |= p . (x,y) )