Description: A single axiom for Boolean algebra known as DN_1. See McCune, Veroff,
Fitelson, Harris, Feist, Wos,Short single axioms for Boolean algebra,
Journal of Automated Reasoning, 29(1):1--16, 2002.
( https://www.cs.unm.edu/~mccune/papers/basax/v12.pdf ). (Contributed by Jeff Hankins, 3-Jul-2009)(Proof shortened by Andrew Salmon, 13-May-2011)(Proof shortened by Wolf Lammen, 6-Jan-2013)