let A, B be MP-wff; :: thesis: ( 'not' A = 'not' B implies A = B )
assume A1: 'not' A = 'not' B ; :: thesis: A = B
<*0*> in dom ((elementary_tree 1) --> [1,0]) by Lm3;
hence A = B by A1, Th7; :: thesis: verum