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