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

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 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