ex a, b being set st
( a in QC-WFF & b in vSUB & [a,b] = Z ) by ZFMISC_1:def 2;
hence Z `2 is CQC_Substitution by MCART_1:7; :: thesis: verum