theorem :: GOEDELCP:7

for Al being QC-alphabet
for p, q 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 implies ( JH, valH Al |= q iff CX |- q ) ) & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p '&' q iff CX |- p '&' q ) by Th6, VALUAT_1:18;