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