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