let Al be QC-alphabet ; :: thesis: for PSI being Subset of (CQC-WFF Al)
for p being Element of CQC-WFF Al st PSI |= p holds
PSI |- p
let PSI be Subset of (CQC-WFF Al); :: thesis: for p being Element of CQC-WFF Al st PSI |= p holds
PSI |- p
let p be Element of CQC-WFF Al; :: thesis: ( PSI |= p implies PSI |- p )
set CHI = PSI \/ {('not' p)};
assume A1: PSI |= p ; :: thesis: PSI |- p
assume not PSI |- p ; :: thesis: contradiction
then PSI \/ {('not' p)} is Consistent by HENMODEL:9;
then ex A being non empty set ex J being interpretation of Al,A ex v being Element of Valuations_in (Al,A) st J,v |= PSI \/ {('not' p)} by Def1;
hence contradiction by GOEDELCP:37, A1; :: thesis: verum