theorem :: HENMODEL:17

for Al being QC-alphabet
for k being Nat
for P being QC-pred_symbol of k,Al
for ll being CQC-variable_list of k,Al
for CX being Consistent Subset of (CQC-WFF Al)
for JH being Henkin_interpretation of CX holds
( JH, valH Al |= P ! ll iff CX |- P ! ll )