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