theorem :: GOEDELCP:1

for Al being QC-alphabet
for p being Element of CQC-WFF Al
for CX being Consistent Subset of (CQC-WFF Al) st CX is negation_faithful holds
( CX |- p iff not CX |- 'not' p ) by HENMODEL:def 2;