set Al2 = [:NAT,(() \/ { [ 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 = () \/ { [ the free_symbol of Al,[x,p]] where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } ;
( [:NAT,(() \/ { [ 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= () \/ { [ the free_symbol of Al,[x,p]] where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } & [:NAT,(() \/ { [ the free_symbol of Al,[x,p]] where p is Element of CQC-WFF Al, x is bound_QC-variable of Al : verum } ):] = [: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 ;
then reconsider Al2 = [:NAT,(() \/ { [ 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,():] c= [:NAT,():] \/ [: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,():] c= [: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 ZFMISC_1:97;
then Al c= Al2 by QC_LANG1:5;
hence [:NAT,(() \/ { [ 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