set Sub = the CQC_Substitution;
set x = the bound_QC-variable;
set B = [[VERUM, the CQC_Substitution], the bound_QC-variable];
reconsider S = [VERUM, the CQC_Substitution] as Element of QC-Sub-WFF by QC_LANG1:def 12, SUBSTUT1:def 16;
[VERUM, the CQC_Substitution] in QC-Sub-WFF by QC_LANG1:def 12, SUBSTUT1:def 16;
then reconsider B = [[VERUM, the CQC_Substitution], the bound_QC-variable] as Element of [:QC-Sub-WFF,bound_QC-variables:] by ZFMISC_1:87;
take B ; :: thesis: B is CQC-WFF-like
S `1 is Element of CQC-WFF by MCART_1:7;
then S in CQC-Sub-WFF by SUBSTUT1:def 39;
then B `1 in CQC-Sub-WFF by MCART_1:7;
hence B is CQC-WFF-like by Def5; :: thesis: verum