let CX be Consistent Subset of CQC-WFF ; :: thesis: ( still_not-bound_in CX is finite implies ex CZ being Consistent Subset of CQC-WFF ex JH1 being Henkin_interpretation of CZ st JH1, valH |= CX )
assume still_not-bound_in CX is finite ; :: thesis: ex CZ being Consistent Subset of CQC-WFF ex JH1 being Henkin_interpretation of CZ st JH1, valH |= CX
then consider CY being Consistent Subset of CQC-WFF such that
A1: CX c= CY and
A2: CY is with_examples by Th31;
consider CZ being Consistent Subset of CQC-WFF such that
A3: CY c= CZ and
A4: CZ is negation_faithful and
A5: CZ is with_examples by A2, Th33;
A6: CX c= CZ by A1, A3, XBOOLE_1:1;
consider JH1 being Henkin_interpretation of CZ;

A7: now

let p be Element of CQC-WFF ; :: thesis: ( p in CX implies JH1, valH |= p )
assume p in CX ; :: thesis: JH1, valH |= p
then CZ |- p by A6, Th21;
hence JH1, valH |= p by A4, A5, Th17; :: thesis: verum

end;

take CZ ; :: thesis: ex JH1 being Henkin_interpretation of CZ st JH1, valH |= CX
take JH1 ; :: thesis: JH1, valH |= CX
thus JH1, valH |= CX by A7, CALCUL_1:def 11; :: thesis: verum