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