let A be QC-alphabet ; :: thesis: for S, S9 being Element of QC-Sub-WFF A st Sub_not S = Sub_not S9 holds
S = S9
let S, S9 be Element of QC-Sub-WFF A; :: 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 XTUPLE_0:1;
( S = [(S `1),(S `2)] & S9 = [(S9 `1),(S9 `2)] ) by Th10;
hence S = S9 by A1, FINSEQ_1:33; :: thesis: verum