let A be QC-alphabet ; :: thesis: ( [:{4},(QC-symbols A):] c= QC-variables A & [:{5},(QC-symbols A):] c= QC-variables A & [:{6},NAT:] c= QC-variables A )
{5} c= {4,5} by ZFMISC_1:7;
then A1: [:{5},(QC-symbols A):] c= [:{4,5},(QC-symbols A):] by ZFMISC_1:96;
{4} c= {4,5} by ZFMISC_1:7;
then [:{4},(QC-symbols A):] c= [:{4,5},(QC-symbols A):] by ZFMISC_1:96;
hence ( [:{4},(QC-symbols A):] c= QC-variables A & [:{5},(QC-symbols A):] c= QC-variables A & [:{6},NAT:] c= QC-variables A ) by A1, XBOOLE_1:10; :: thesis: verum