let Al be QC-alphabet ; :: thesis: for CX being Consistent Subset of (CQC-WFF Al)
for JH being Henkin_interpretation of CX
for p being Element of CQC-WFF Al st CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p )
let CX be Consistent Subset of (CQC-WFF Al); :: thesis: for JH being Henkin_interpretation of CX
for p being Element of CQC-WFF Al st CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p )
let JH be Henkin_interpretation of CX; :: thesis: for p being Element of CQC-WFF Al st CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p )
defpred S₁[ Element of CQC-WFF Al] means ( CX is negation_faithful & CX is with_examples implies ( JH, valH Al |= $1 iff CX |- $1 ) );
A1: for p being Element of CQC-WFF Al st QuantNbr p <= 0 holds
S₁[p] by Th8;
A2: for k being Nat st ( for p being Element of CQC-WFF Al st QuantNbr p <= k holds
S₁[p] ) holds
for p being Element of CQC-WFF Al st QuantNbr p <= k + 1 holds
S₁[p] by Th16;
thus for p being Element of CQC-WFF Al holds S₁[p] from SUBSTUT2:sch 2(A1, A2); :: thesis: verum