let Al be QC-alphabet ; :: thesis: for PHI being finite Subset of (CQC-WFF Al) ex Al1 being countable QC-alphabet st
( PHI is finite Subset of (CQC-WFF Al1) & Al is Al1 -expanding )

let PHI be finite Subset of (CQC-WFF Al); :: thesis: ex Al1 being countable QC-alphabet st
( PHI is finite Subset of (CQC-WFF Al1) & Al is Al1 -expanding )

defpred S1[ set ] means ( \$1 is finite Subset of (CQC-WFF Al) implies ex Al1 being countable QC-alphabet st
( \$1 is finite Subset of (CQC-WFF Al1) & Al is Al1 -expanding ) );
A1: PHI is finite ;
A2: S1[ {} ]
proof
set Al1 = ;
reconsider Al1 = as countable QC-alphabet by ;
( Al = [:NAT,():] & NAT c= QC-symbols Al ) by ;
then ( Al is Al1 -expanding & {} is finite Subset of (CQC-WFF Al1) ) by ;
hence S1[ {} ] ; :: thesis: verum
end;
A3: for x, B being set st x in PHI & B c= PHI & S1[B] holds
S1[B \/ {x}]
proof
let x, B be set ; :: thesis: ( x in PHI & B c= PHI & S1[B] implies S1[B \/ {x}] )
assume A4: ( x in PHI & B c= PHI & S1[B] ) ; :: thesis: S1[B \/ {x}]
reconsider x = x as Element of CQC-WFF Al by A4;
reconsider B = B as finite Subset of (CQC-WFF Al) by ;
consider Al1 being countable QC-alphabet such that
A5: ( x is Element of CQC-WFF Al1 & Al is Al1 -expanding ) by Th19;
consider Al2 being countable QC-alphabet such that
A6: ( B is finite Subset of (CQC-WFF Al2) & Al is Al2 -expanding ) by A4;
set Al3 = Al1 \/ Al2;
( Al1 = [:NAT,(QC-symbols Al1):] & Al2 = [:NAT,(QC-symbols Al2):] ) by QC_LANG1:5;
then A7: Al1 \/ Al2 = [:NAT,((QC-symbols Al1) \/ (QC-symbols Al2)):] by ZFMISC_1:97;
NAT c= (QC-symbols Al1) \/ (QC-symbols Al2) by ;
then reconsider Al3 = Al1 \/ Al2 as QC-alphabet by ;
reconsider Al3 = Al3 as countable Al1 -expanding Al2 -expanding QC-alphabet by ;
consider x2 being Element of CQC-WFF Al1 such that
A8: x = x2 by A5;
for s being object st s in B holds
s in CQC-WFF Al3
proof
let s be object ; :: thesis: ( s in B implies s in CQC-WFF Al3 )
assume A9: s in B ; :: thesis: s in CQC-WFF Al3
consider s2 being Element of CQC-WFF Al2 such that
A10: s = s2 by A6, A9;
s2 is Element of CQC-WFF Al3 by Th7;
hence s in CQC-WFF Al3 by A10; :: thesis: verum
end;
then ( x2 is Element of CQC-WFF Al3 & B c= CQC-WFF Al3 ) by Th7;
then ( {x2} c= CQC-WFF Al3 & B c= CQC-WFF Al3 ) by ZFMISC_1:31;
then A11: B \/ {x} c= CQC-WFF Al3 by ;
( Al1 c= Al & Al2 c= Al ) by A5, A6;
then Al is Al3 -expanding QC-alphabet by ;
hence S1[B \/ {x}] by A11; :: thesis: verum
end;
S1[PHI] from FINSET_1:sch 2(A1, A2, A3);
hence ex Al1 being countable QC-alphabet st
( PHI is finite Subset of (CQC-WFF Al1) & Al is Al1 -expanding ) ; :: thesis: verum