consider Sub being CQC_Substitution, x being bound_QC-variable;
set B = [[VERUM,Sub],x];
reconsider S = [VERUM,Sub] as Element of QC-Sub-WFF by QC_LANG1:def 13, SUBSTUT1:def 16;
[VERUM,Sub] in QC-Sub-WFF by QC_LANG1:def 13, SUBSTUT1:def 16;
then reconsider B = [[VERUM,Sub],x] as Element of [:QC-Sub-WFF,bound_QC-variables:] by ZFMISC_1:106;
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