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