set e = the Element of vSUB ;
reconsider S = [VERUM, the Element of vSUB ] as Element of QC-Sub-WFF by Def16;
S `1 = VERUM by MCART_1:7;
then [VERUM, the Element of vSUB ] in CQC-Sub-WFF ;
hence not CQC-Sub-WFF is empty ; :: thesis: verum