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