set Al2 = FCEx Al;
[:NAT,(QC-symbols (FCEx Al)):] = [:NAT,((QC-symbols Al) \/ { [ the free_symbol of Al,[y,q]] where q is Element of CQC-WFF Al, y is bound_QC-variable of Al : verum } ):]
by QC_LANG1:5;
then A1:
QC-symbols (FCEx Al) = (QC-symbols Al) \/ { [ the free_symbol of Al,[y,q]] where q is Element of CQC-WFF Al, y is bound_QC-variable of Al : verum }
by ZFMISC_1:110;
[ the free_symbol of Al,[x,p]] in { [ the free_symbol of Al,[y,q]] where q is Element of CQC-WFF Al, y is bound_QC-variable of Al : verum }
;
then A2:
[ the free_symbol of Al,[x,p]] in QC-symbols (FCEx Al)
by A1, XBOOLE_0:def 3;
4 in {4}
by TARSKI:def 1;
then
[4,[ the free_symbol of Al,[x,p]]] in [:{4},(QC-symbols (FCEx Al)):]
by A2, ZFMISC_1:87;
hence
[4,[ the free_symbol of Al,[x,p]]] is bound_QC-variable of (FCEx Al)
by QC_LANG1:def 4; verum