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

proof

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;

hence PSI is Consistent by HENMODEL:7; :: thesis: verum