let Al be QC-alphabet ; :: thesis: for CX being Consistent Subset of (CQC-WFF Al) st Al is countable & still_not-bound_in CX is finite holds
ex CZ being Consistent Subset of (CQC-WFF Al) ex JH1 being Henkin_interpretation of CZ st JH1, valH Al |= CX
let CX be Consistent Subset of (CQC-WFF Al); :: thesis: ( Al is countable & still_not-bound_in CX is finite implies ex CZ being Consistent Subset of (CQC-WFF Al) ex JH1 being Henkin_interpretation of CZ st JH1, valH Al |= CX )
assume A1: Al is countable ; :: thesis: ( not still_not-bound_in CX is finite or ex CZ being Consistent Subset of (CQC-WFF Al) ex JH1 being Henkin_interpretation of CZ st JH1, valH Al |= CX )
assume still_not-bound_in CX is finite ; :: thesis: ex CZ being Consistent Subset of (CQC-WFF Al) ex JH1 being Henkin_interpretation of CZ st JH1, valH Al |= CX
then consider CY being Consistent Subset of (CQC-WFF Al) such that
A2: CX c= CY and
A3: CY is with_examples by Th31, A1;
consider CZ being Consistent Subset of (CQC-WFF Al) such that
A4: CY c= CZ and
A5: CZ is negation_faithful and
A6: CZ is with_examples by A1, A3, Th33;
A7: CX c= CZ by A2, A4;
set JH1 = the Henkin_interpretation of CZ;
A8: now :: thesis: for p being Element of CQC-WFF Al st p in CX holds
the Henkin_interpretation of CZ, valH Al |= p
let p be Element of CQC-WFF Al; :: thesis: ( p in CX implies the Henkin_interpretation of CZ, valH Al |= p )
assume p in CX ; :: thesis: the Henkin_interpretation of CZ, valH Al |= p
then CZ |- p by A7, Th21;
hence the Henkin_interpretation of CZ, valH Al |= p by A5, A6, Th17; :: thesis: verum
end;
take CZ ; :: thesis: ex JH1 being Henkin_interpretation of CZ st JH1, valH Al |= CX
take the Henkin_interpretation of CZ ; :: thesis: the Henkin_interpretation of CZ, valH Al |= CX
thus the Henkin_interpretation of CZ, valH Al |= CX by A8, CALCUL_1:def 11; :: thesis: verum