theorem Th8: :: GOEDELCP:8

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 QuantNbr p <= 0 & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p )