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