let Al be 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 )
let k be 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 )
let P be 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 )
let ll be 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 )
let CX be Consistent Subset of (CQC-WFF Al); for JH being Henkin_interpretation of CX holds
( JH, valH Al |= P ! ll iff CX |- P ! ll )
let JH be Henkin_interpretation of CX; ( JH, valH Al |= P ! ll iff CX |- P ! ll )
thus
( JH, valH Al |= P ! ll implies CX |- P ! ll )
( CX |- P ! ll implies JH, valH Al |= P ! ll )
thus
( CX |- P ! ll implies JH, valH Al |= P ! ll )
verum