閉じたにこだわらず別に
　∀x(x+0'=x')
の代わりに
　x+0'=x'
が入っていてもかまわんよ