let Al be QC-alphabet ; 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); for Al2 being Al -expanding QC-alphabet holds PHI is Al2 -Consistent
let Al2 be Al -expanding QC-alphabet ; PHI is Al2 -Consistent
let PSI be Subset of (CQC-WFF Al2); QC_TRANS:def 2 ( PHI = PSI implies PSI is Consistent )
assume A1:
PHI = PSI
; 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);
( CHI c= PSI & CHI is finite implies CHI is Consistent )
assume A2:
(
CHI c= PSI &
CHI is
finite )
;
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;
verum
end;
hence
PSI is Consistent
by HENMODEL:7; verum