set Al2 = [:NAT,((QC-symbols Al) \/ { [ the free_symbol of Al,[x,p]] where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } ):];

set X = (QC-symbols Al) \/ { [ the free_symbol of Al,[x,p]] where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } ;

( [:NAT,((QC-symbols Al) \/ { [ the free_symbol of Al,[x,p]] where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } ):] is non empty set & NAT c= (QC-symbols Al) \/ { [ the free_symbol of Al,[x,p]] where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } & [:NAT,((QC-symbols Al) \/ { [ the free_symbol of Al,[x,p]] where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } ):] = [:NAT,((QC-symbols Al) \/ { [ the free_symbol of Al,[x,p]] where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } ):] ) by QC_LANG1:3, XBOOLE_1:10;

then reconsider Al2 = [:NAT,((QC-symbols Al) \/ { [ the free_symbol of Al,[x,p]] where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } ):] as QC-alphabet by QC_LANG1:def 1;

[:NAT,(QC-symbols Al):] c= [:NAT,(QC-symbols Al):] \/ [:NAT, { [ the free_symbol of Al,[x,p]] where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } :] by XBOOLE_1:7;

then [:NAT,(QC-symbols Al):] c= [:NAT,((QC-symbols Al) \/ { [ the free_symbol of Al,[x,p]] where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } ):] by ZFMISC_1:97;

then Al c= Al2 by QC_LANG1:5;

hence [:NAT,((QC-symbols Al) \/ { [ the free_symbol of Al,[x,p]] where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } ):] is Al -expanding QC-alphabet by QC_TRANS:def 1; :: thesis: verum

set X = (QC-symbols Al) \/ { [ the free_symbol of Al,[x,p]] where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } ;

( [:NAT,((QC-symbols Al) \/ { [ the free_symbol of Al,[x,p]] where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } ):] is non empty set & NAT c= (QC-symbols Al) \/ { [ the free_symbol of Al,[x,p]] where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } & [:NAT,((QC-symbols Al) \/ { [ the free_symbol of Al,[x,p]] where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } ):] = [:NAT,((QC-symbols Al) \/ { [ the free_symbol of Al,[x,p]] where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } ):] ) by QC_LANG1:3, XBOOLE_1:10;

then reconsider Al2 = [:NAT,((QC-symbols Al) \/ { [ the free_symbol of Al,[x,p]] where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } ):] as QC-alphabet by QC_LANG1:def 1;

[:NAT,(QC-symbols Al):] c= [:NAT,(QC-symbols Al):] \/ [:NAT, { [ the free_symbol of Al,[x,p]] where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } :] by XBOOLE_1:7;

then [:NAT,(QC-symbols Al):] c= [:NAT,((QC-symbols Al) \/ { [ the free_symbol of Al,[x,p]] where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } ):] by ZFMISC_1:97;

then Al c= Al2 by QC_LANG1:5;

hence [:NAT,((QC-symbols Al) \/ { [ the free_symbol of Al,[x,p]] where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } ):] is Al -expanding QC-alphabet by QC_TRANS:def 1; :: thesis: verum