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