let S, S9 be Element of QC-Sub-WFF ; :: thesis: ( Sub_not S = Sub_not S9 implies S = S9 )
assume Sub_not S = Sub_not S9 ; :: thesis: S = S9
then A1: ( 'not' (S `1 ) = 'not' (S9 `1 ) & S `2 = S9 `2 ) by ZFMISC_1:33;
( S = [(S `1 ),(S `2 )] & S9 = [(S9 `1 ),(S9 `2 )] ) by Th10;
hence S = S9 by A1, FINSEQ_1:46; :: thesis: verum