let Al be QC-alphabet ; :: thesis: for Al2 being Al -expanding QC-alphabet holds bound_QC-variables Al c= bound_QC-variables Al2
let Al2 be Al -expanding QC-alphabet ; :: thesis: bound_QC-variables Al c= bound_QC-variables Al2
A1: QC-symbols Al c= QC-symbols Al2 by Th2;
thus bound_QC-variables Al c= bound_QC-variables Al2 by A1, ZFMISC_1:96; :: thesis: verum