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