set Sub = the CQC_Substitution of Al;
set x = the bound_QC-variable of Al;
set B = [[(VERUM Al), the CQC_Substitution of Al], the bound_QC-variable of Al];
A1: VERUM Al = <*[0,0]*> by QC_LANG1:def 14;
A2: [<*[0,0]*>, the CQC_Substitution of Al] in QC-Sub-WFF Al by SUBSTUT1:def 16;
reconsider S = [(VERUM Al), the CQC_Substitution of Al] as Element of QC-Sub-WFF Al by A1, SUBSTUT1:def 16;
[(VERUM Al), the CQC_Substitution of Al] in QC-Sub-WFF Al by A2, QC_LANG1:def 14;
then reconsider B = [[(VERUM Al), the CQC_Substitution of Al], the bound_QC-variable of Al] as Element of [:(QC-Sub-WFF Al),(bound_QC-variables Al):] by ZFMISC_1:87;
take B ; :: thesis: B is CQC-WFF-like
set X = { G where G is Element of QC-Sub-WFF Al : G `1 is Element of CQC-WFF Al } ;
A3: { G where G is Element of QC-Sub-WFF Al : G `1 is Element of CQC-WFF Al } = CQC-Sub-WFF Al by SUBSTUT1:def 39;
S `1 is Element of CQC-WFF Al ;
then S in CQC-Sub-WFF Al by A3;
then B `1 in CQC-Sub-WFF Al ;
hence B is CQC-WFF-like ; :: thesis: verum