consider a, b being set such that
A2: ( a in QC-WFF & b in vSUB & [a,b] = Z ) by ZFMISC_1:def 2;
thus Z `2 is CQC_Substitution by A2, MCART_1:7; :: thesis: verum