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