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

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