( [(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