I am analysing axiomatic approach to defining real numbers. There are two axioms that postulate existence of $0$ and $1$, namely (according to my notes):
There exists an element $0\in\mathbb{R}$ such that for any $x\in\mathbb{R}$ we have $x+0=x.$
There exists an element $1\in\mathbb{R}$ such that for any $x\in\mathbb{R}$ we have $x\times 1=x$.
Then, I see a really little remark, almost non-existent, that says
We suppose $1\neq 0$.
I searched other sources which provided basically the same axioms but nowhere I could see the sentence $1\neq 0$ as an axiom.
My question is - why isn't it considered as an separate axiom? What it is then? I don't think you can prove it from other axioms of $\mathbb{R}$ and I think it is fairly important for the whole theory to work properly.