let k be Element of NAT ; :: thesis: for P being QC-pred_symbol of k
for ll being CQC-variable_list of
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
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 ; :: 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

assume A1: JH, valH |= P ! ll ; :: thesis: CX |- P ! ll
set rel = JH . P;
reconsider rel = JH . P as Element of relations_on HCar ;
(Valid (P ! ll),JH) . valH = TRUE by A1, VALUAT_1:def 12;
then valH *' ll in rel by VALUAT_1:16;
then ll in rel by Th14;
then consider ll' being CQC-variable_list of such that
A2: ( ll' = ll & CX |- P ! ll' ) by Def6;
thus CX |- P ! ll by A2; :: thesis: verum

end;

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

proof

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

end;