let Al be QC-alphabet ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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); :: thesis: for JH being Henkin_interpretation of CX holds

( JH, valH Al |= P ! ll iff CX |- P ! ll )

let JH be Henkin_interpretation of CX; :: thesis: ( JH, valH Al |= P ! ll iff CX |- P ! ll )

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

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; :: thesis: 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; :: thesis: 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; :: thesis: 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); :: thesis: for JH being Henkin_interpretation of CX holds

( JH, valH Al |= P ! ll iff CX |- P ! ll )

let JH be Henkin_interpretation of CX; :: thesis: ( JH, valH Al |= P ! ll iff CX |- P ! ll )

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

proof

thus
( CX |- P ! ll implies JH, valH Al |= P ! ll )
:: thesis: verum
set rel = JH . P;

reconsider rel = JH . P as Element of relations_on (HCar Al) ;

assume JH, valH Al |= P ! ll ; :: thesis: CX |- P ! ll

then (Valid ((P ! ll),JH)) . (valH Al) = TRUE by VALUAT_1:def 7;

then (valH Al) *' 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,Al st

( ll9 = ll & CX |- P ! ll9 ) by Def5;

hence CX |- P ! ll ; :: thesis: verum

end;reconsider rel = JH . P as Element of relations_on (HCar Al) ;

assume JH, valH Al |= P ! ll ; :: thesis: CX |- P ! ll

then (Valid ((P ! ll),JH)) . (valH Al) = TRUE by VALUAT_1:def 7;

then (valH Al) *' 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,Al st

( ll9 = ll & CX |- P ! ll9 ) by Def5;

hence CX |- P ! ll ; :: thesis: verum

proof

P is QC-pred_symbol of (the_arity_of P),Al
by QC_LANG3:1;

then A1: the_arity_of P = k by SUBSTUT2:3;

assume CX |- P ! ll ; :: thesis: JH, valH Al |= P ! ll

then ll in JH . P by A1, Def5;

then (valH Al) *' ll in JH . P by Th14;

then (Valid ((P ! ll),JH)) . (valH Al) = TRUE by VALUAT_1:7;

hence JH, valH Al |= P ! ll by VALUAT_1:def 7; :: thesis: verum

end;then A1: the_arity_of P = k by SUBSTUT2:3;

assume CX |- P ! ll ; :: thesis: JH, valH Al |= P ! ll

then ll in JH . P by A1, Def5;

then (valH Al) *' ll in JH . P by Th14;

then (Valid ((P ! ll),JH)) . (valH Al) = TRUE by VALUAT_1:7;

hence JH, valH Al |= P ! ll by VALUAT_1:def 7; :: thesis: verum