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