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