let X be Subset of CQC-WFF; :: thesis: for p being Element of CQC-WFF st still_not-bound_in X is finite & X |= p holds
X |- p
let p be Element of CQC-WFF ; :: thesis: ( still_not-bound_in X is finite & X |= p implies X |- p )
assume A1: still_not-bound_in X is finite ; :: thesis: ( not X |= p or X |- p )
assume A2: X |= p ; :: thesis: X |- p
assume A3: not X |- p ; :: thesis: contradiction
reconsider Y = X \/ {('not' p)} as Subset of CQC-WFF ;
A4: still_not-bound_in Y is finite by A1, Th36;
Y is Consistent by A3, HENMODEL:9;
then ex CZ being Consistent Subset of CQC-WFF ex JH1 being Henkin_interpretation of CZ st JH1, valH |= Y by A4, Th34;
hence contradiction by A2, Th37; :: thesis: verum