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