let k be Element of NAT ; :: thesis: for P being QC-pred_symbol of k
for ll being CQC-variable_list of k
for CX being Consistent Subset of CQC-WFF
for JH being Henkin_interpretation of CX holds
( JH, valH |= P ! ll iff CX |- P ! ll )
let P be QC-pred_symbol of k; :: thesis: for ll being CQC-variable_list of k
for CX being Consistent Subset of CQC-WFF
for JH being Henkin_interpretation of CX holds
( JH, valH |= P ! ll iff CX |- P ! ll )
let ll be CQC-variable_list of k; :: thesis: for CX being Consistent Subset of CQC-WFF
for JH being Henkin_interpretation of CX holds
( JH, valH |= P ! ll iff CX |- P ! ll )
let CX be Consistent Subset of CQC-WFF; :: thesis: for JH being Henkin_interpretation of CX holds
( JH, valH |= P ! ll iff CX |- P ! ll )
let JH be Henkin_interpretation of CX; :: thesis: ( JH, valH |= P ! ll iff CX |- P ! ll )
thus ( JH, valH |= P ! ll implies CX |- P ! ll ) :: thesis: ( CX |- P ! ll implies JH, valH |= P ! ll )

proof

set rel = JH . P;
reconsider rel = JH . P as Element of relations_on HCar ;
assume JH, valH |= P ! ll ; :: thesis: CX |- P ! ll
then (Valid ((P ! ll),JH)) . valH = TRUE by VALUAT_1:def 7;
then valH *' ll in rel by VALUAT_1:7;
then ll in rel by Th14;
then ex ll9 being CQC-variable_list of the_arity_of P st
( ll9 = ll & CX |- P ! ll9 ) by Def6;
hence CX |- P ! ll ; :: thesis: verum

end;

thus ( CX |- P ! ll implies JH, valH |= P ! ll ) :: thesis: verum

proof

P is QC-pred_symbol of (the_arity_of P) by QC_LANG3:1;
then A1: the_arity_of P = k by SUBSTUT2:3;
assume CX |- P ! ll ; :: thesis: JH, valH |= P ! ll
then ll in JH . P by A1, Def6;
then valH *' ll in JH . P by Th14;
then (Valid ((P ! ll),JH)) . valH = TRUE by VALUAT_1:7;
hence JH, valH |= P ! ll by VALUAT_1:def 7; :: thesis: verum

end;