let S be Element of QC-Sub-WFF ; :: thesis: S = [(S `1),(S `2)]
ex p being QC-formula ex e being Element of vSUB st S = [p,e] by Th8;
hence S = [(S `1),(S `2)] by MCART_1:8; :: thesis: verum