( [(S `1),(S `2)] is Element of QC-Sub-WFF & [(S9 `1),(S9 `2)] is Element of QC-Sub-WFF ) by Th10;
hence [((S `1) '&' (S9 `1)),(S `2)] is Element of QC-Sub-WFF by A1, Def16; :: thesis: verum