definitions: use ([acronym]1), ([acronym]2), etc. If the axioms resemble an existing structure, use their naming instead.

Set builders must use bar.

(U) indicates some kind of universal property, or some kind of property that makes this object unique.

$\natp = \bracs{1, \cdots}$, $\nat_0 = \bracs{0, 1, \cdots}$. Nobody knows what $\nat$ is.