let A be QC-alphabet ; ( [:{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; verum