[pedagogical]
We translate the proof of the theorem stated in the title, accomplished by Prover9, into a human readable form.
https://doi.org/10.31219/osf.io/wsbne
Open Mathematics Collaboration
Op. J. Math. Phys.
Volume 3, Article 222, 2021 [IS]