let Al be QC-alphabet ; :: thesis: for PHI being Consistent Subset of (CQC-WFF Al)

for CHI being Subset of (CQC-WFF Al) st CHI c= PHI holds

CHI is Consistent

let PHI be Consistent Subset of (CQC-WFF Al); :: thesis: for CHI being Subset of (CQC-WFF Al) st CHI c= PHI holds

CHI is Consistent

let CHI be Subset of (CQC-WFF Al); :: thesis: ( CHI c= PHI implies CHI is Consistent )

assume A1: CHI c= PHI ; :: thesis: CHI is Consistent

assume CHI is Inconsistent ; :: thesis: contradiction

then ex f being FinSequence of CQC-WFF Al st

( rng f c= CHI & |- f ^ <*('not' (VERUM Al))*> ) by HENMODEL:def 1, GOEDELCP:24;

then PHI |- 'not' (VERUM Al) by A1, HENMODEL:def 1, XBOOLE_1:1;

hence contradiction by GOEDELCP:24; :: thesis: verum

for CHI being Subset of (CQC-WFF Al) st CHI c= PHI holds

CHI is Consistent

let PHI be Consistent Subset of (CQC-WFF Al); :: thesis: for CHI being Subset of (CQC-WFF Al) st CHI c= PHI holds

CHI is Consistent

let CHI be Subset of (CQC-WFF Al); :: thesis: ( CHI c= PHI implies CHI is Consistent )

assume A1: CHI c= PHI ; :: thesis: CHI is Consistent

assume CHI is Inconsistent ; :: thesis: contradiction

then ex f being FinSequence of CQC-WFF Al st

( rng f c= CHI & |- f ^ <*('not' (VERUM Al))*> ) by HENMODEL:def 1, GOEDELCP:24;

then PHI |- 'not' (VERUM Al) by A1, HENMODEL:def 1, XBOOLE_1:1;

hence contradiction by GOEDELCP:24; :: thesis: verum