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