ex p being QC-formula of A ex e being Element of vSUB A st S = [p,e] by Th8;
hence S is Element of [:(QC-WFF A),(vSUB A):] ; :: thesis: verum