consider p being QC-formula, e being Element of vSUB such that
A1: S = [p,e] by Th8;
thus S is Element of [:QC-WFF ,vSUB :] by A1; :: thesis: verum