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