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 S₁[ 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: S₁[ {} ]

proof

set Al1 = [:NAT,NAT:];
reconsider Al1 = [:NAT,NAT:] as countable QC-alphabet by QC_LANG1:def 1, CARD_4:7;
( Al = [:NAT,(QC-symbols Al):] & NAT c= QC-symbols Al ) by QC_LANG1:3, QC_LANG1:5;
then ( Al is Al1 -expanding & {} is finite Subset of (CQC-WFF Al1) ) by XBOOLE_1:2, ZFMISC_1:96;
hence S₁[ {} ] ; :: thesis: verum

end;

A3: for x, B being set st x in PHI & B c= PHI & S₁[B] holds
S₁[B \/ {x}]

proof

let x, B be set ; :: thesis: ( x in PHI & B c= PHI & S₁[B] implies S₁[B \/ {x}] )
assume A4: ( x in PHI & B c= PHI & S₁[B] ) ; :: thesis: S₁[B \/ {x}]
reconsider x = x as Element of CQC-WFF Al by A4;
reconsider B = B as finite Subset of (CQC-WFF Al) by A4, XBOOLE_1:1;
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 QC_LANG1:3, XBOOLE_1:10;
then reconsider Al3 = Al1 \/ Al2 as QC-alphabet by A7, QC_LANG1:def 1;
reconsider Al3 = Al3 as countable Al1 -expanding Al2 -expanding QC-alphabet by Def1, CARD_2:85, XBOOLE_1:7;
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 A8, XBOOLE_1:8;
( Al1 c= Al & Al2 c= Al ) by A5, A6;
then Al is Al3 -expanding QC-alphabet by Def1, XBOOLE_1:8;
hence S₁[B \/ {x}] by A11; :: thesis: verum

end;

S₁[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