This proof is more of a test to see whether this obvious theorem can be derived from simpler axioms or if it need to be a axiom itself.