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 & CY is with_examples ) by Th31;
consider CZ being Consistent Subset of CQC-WFF such that
A2: ( CY c= CZ & CZ is negation_faithful & CZ is with_examples ) by A1, Th33;
A3: CX c= CZ by A1, A2, XBOOLE_1:1;
consider JH1 being Henkin_interpretation of CZ;

A4: now

let p be Element of CQC-WFF ; :: thesis: ( p in CX implies JH1, valH |= p )
assume A5: p in CX ; :: thesis: JH1, valH |= p
CZ |- p by A3, A5, Th21;
hence JH1, valH |= p by A2, 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 A4, CALCUL_1:def 11; :: thesis: verum