Profinite groups are usually characterized as compact, totally disconnected, Hausdorff groups. However, as shown here, every totally disconnected topological group already has the Hausdorff property.
Still, every textbook I've come across explicitly mentions (and even proves) the Hausdorff property in the characterization. Is there any reason whatsoever for this emphasis?
Yes it is quite funny that every totally disconnected topological group is automatically Hausdorff.
There are more places in mathematics where this superfluousness is present. For example the definition of a (left) module $M$ over a ring $R$ with identity $1$. In every textbook $M$ is required to be an abelian group, but it is implied by the axioms: $r(m_1+m_2)=rm_1+rm_2$ en $(r_1+r_2)m=r_1m+r_2m$. For these yield $(1+1)(m_1+m_2)=m_1+m_1+m_2+m_2$ and also $(1+1)(m_1+m_2)=m_1+m_2+m_1+m_2$, whence $m_1+m_2=m_2+m_1$!
So I guess it is laziness or a matter of ease.