let Al be QC-alphabet ; :: thesis: for Al2 being Al -expanding QC-alphabet holds QC-symbols Al c= QC-symbols Al2
let Al2 be Al -expanding QC-alphabet ; :: thesis: QC-symbols Al c= QC-symbols Al2
( Al c= Al2 & Al = [:NAT,(QC-symbols Al):] & Al2 = [:NAT,(QC-symbols Al2):] ) by Def1, QC_LANG1:5;
hence QC-symbols Al c= QC-symbols Al2 by ZFMISC_1:115; :: thesis: verum