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 QuantNbr p <= 0 & 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 QuantNbr p <= 0 & 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 QuantNbr p <= 0 & 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 r, s being Element of CQC-WFF Al
for x being bound_QC-variable of Al
for k being Nat
for l being CQC-variable_list of k,Al
for P being QC-pred_symbol of k,Al holds
( S₁[ VERUM Al] & S₁[P ! l] & ( S₁[r] implies S₁[ 'not' r] ) & ( S₁[r] & S₁[s] implies S₁[r '&' s] ) ) by Def1, Th6, HENMODEL:16, HENMODEL:17, HENMODEL:def 2, VALUAT_1:17, VALUAT_1:18;
A2: for p being Element of CQC-WFF Al st QuantNbr p = 0 holds
S₁[p] from SUBSTUT2:sch 3(A1);

now :: thesis: for p being Element of CQC-WFF Al st QuantNbr p <= 0 holds
S₁[p]

let p be Element of CQC-WFF Al; :: thesis: ( QuantNbr p <= 0 implies S₁[p] )
assume QuantNbr p <= 0 ; :: thesis: S₁[p]
then QuantNbr p = 0 by NAT_1:2;
hence S₁[p] by A2; :: thesis: verum

end;

hence for p being Element of CQC-WFF Al st QuantNbr p <= 0 & CX is negation_faithful & CX is with_examples holds
( JH, valH Al |= p iff CX |- p ) ; :: thesis: verum