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