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