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