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
; 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
; verum