consider p being QC-formula, e being Element of vSUB such that
A2: S = [p,e] by Th8;
thus S `2 is Element of vSUB by A2, MCART_1:7; :: thesis: verum