theorem :: GOEDELCP:4

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for CX being Consistent Subset of (CQC-WFF Al)
for JH being Henkin_interpretation of CX st ( CX is negation_faithful & CX is with_examples implies ( JH, valH Al |= p iff CX |- p ) ) & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= 'not' p iff CX |- 'not' p ) by HENMODEL:def 2, VALUAT_1:17;