theorem Th17: :: GOEDELCP:17

for Al being QC-alphabet
for CX being Consistent Subset of (CQC-WFF Al)
for JH being Henkin_interpretation of CX
for p being Element of CQC-WFF Al st CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p )