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