for A, B being MP-wff st 'not' A = 'not' B holds
A = B