let S1, S2 be Element of QC-Sub-WFF A; :: 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 XTUPLE_0:1;
then S1 `1 = S2 `1 by FINSEQ_1:33;
hence S1 = S2 by A3, A2, XTUPLE_0:1; :: thesis: verum