take [:QC-WFF,vSUB:] ; :: thesis: ( [:QC-WFF,vSUB:] is QC-Sub-closed & not [:QC-WFF,vSUB:] is empty )
thus ( [:QC-WFF,vSUB:] is QC-Sub-closed & not [:QC-WFF,vSUB:] is empty ) by Def16, Th7; :: thesis: verum