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

for Al2 being Al -expanding QC-alphabet holds PHI is Al2 -Consistent

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

let Al2 be Al -expanding QC-alphabet ; :: thesis: PHI is Al2 -Consistent

let PSI be Subset of (CQC-WFF Al2); :: according to QC_TRANS:def 2 :: thesis: ( PHI = PSI implies PSI is Consistent )

assume A1: PHI = PSI ; :: thesis: PSI is Consistent

for CHI being Subset of (CQC-WFF Al2) st CHI c= PSI & CHI is finite holds

CHI is Consistent

for Al2 being Al -expanding QC-alphabet holds PHI is Al2 -Consistent

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

let Al2 be Al -expanding QC-alphabet ; :: thesis: PHI is Al2 -Consistent

let PSI be Subset of (CQC-WFF Al2); :: according to QC_TRANS:def 2 :: thesis: ( PHI = PSI implies PSI is Consistent )

assume A1: PHI = PSI ; :: thesis: PSI is Consistent

for CHI being Subset of (CQC-WFF Al2) st CHI c= PSI & CHI is finite holds

CHI is Consistent

proof

hence
PSI is Consistent
by HENMODEL:7; :: thesis: verum
let CHI be Subset of (CQC-WFF Al2); :: thesis: ( CHI c= PSI & CHI is finite implies CHI is Consistent )

assume A2: ( CHI c= PSI & CHI is finite ) ; :: thesis: CHI is Consistent

reconsider CHI = CHI as finite Subset of (CQC-WFF Al) by A1, A2, XBOOLE_1:1;

consider Al1 being countable QC-alphabet such that

A3: ( CHI is finite Subset of (CQC-WFF Al1) & Al is Al1 -expanding ) by Th20;

reconsider Al = Al as Al1 -expanding QC-alphabet by A3;

reconsider CHI = CHI as finite Subset of (CQC-WFF Al) ;

reconsider PHI = PHI as Consistent Subset of (CQC-WFF Al) ;

reconsider CHI = CHI as Consistent Subset of (CQC-WFF Al) by A1, A2, Th22;

CHI is Al1 -Consistent by Th18;

then reconsider CHI = CHI as Consistent Subset of (CQC-WFF Al1) by A3;

still_not-bound_in CHI is finite ;

then consider CZ being Consistent Subset of (CQC-WFF Al1), JH being Henkin_interpretation of CZ such that

A4: JH, valH Al1 |= CHI by GOEDELCP:34;

( Al1 c= Al & Al c= Al2 ) by Def1;

then reconsider Al2 = Al2 as Al1 -expanding QC-alphabet by Def1, XBOOLE_1:1;

consider CHI2 being Subset of (CQC-WFF Al2) such that

A5: CHI = CHI2 ;

ex A being non empty set ex J2 being interpretation of Al2,A ex v2 being Element of Valuations_in (Al2,A) st J2,v2 |= CHI2 by A4, A5, Th21;

hence CHI is Consistent by A5, HENMODEL:12; :: thesis: verum

end;assume A2: ( CHI c= PSI & CHI is finite ) ; :: thesis: CHI is Consistent

reconsider CHI = CHI as finite Subset of (CQC-WFF Al) by A1, A2, XBOOLE_1:1;

consider Al1 being countable QC-alphabet such that

A3: ( CHI is finite Subset of (CQC-WFF Al1) & Al is Al1 -expanding ) by Th20;

reconsider Al = Al as Al1 -expanding QC-alphabet by A3;

reconsider CHI = CHI as finite Subset of (CQC-WFF Al) ;

reconsider PHI = PHI as Consistent Subset of (CQC-WFF Al) ;

reconsider CHI = CHI as Consistent Subset of (CQC-WFF Al) by A1, A2, Th22;

CHI is Al1 -Consistent by Th18;

then reconsider CHI = CHI as Consistent Subset of (CQC-WFF Al1) by A3;

still_not-bound_in CHI is finite ;

then consider CZ being Consistent Subset of (CQC-WFF Al1), JH being Henkin_interpretation of CZ such that

A4: JH, valH Al1 |= CHI by GOEDELCP:34;

( Al1 c= Al & Al c= Al2 ) by Def1;

then reconsider Al2 = Al2 as Al1 -expanding QC-alphabet by Def1, XBOOLE_1:1;

consider CHI2 being Subset of (CQC-WFF Al2) such that

A5: CHI = CHI2 ;

ex A being non empty set ex J2 being interpretation of Al2,A ex v2 being Element of Valuations_in (Al2,A) st J2,v2 |= CHI2 by A4, A5, Th21;

hence CHI is Consistent by A5, HENMODEL:12; :: thesis: verum