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