theorem :: HENMODEL:16

for Al being QC-alphabet
for CX being Consistent Subset of (CQC-WFF Al)
for JH being Henkin_interpretation of CX holds
( JH, valH Al |= VERUM Al iff CX |- VERUM Al )