Suppose we have n objects 
, and we want to assert
that they are all distinct. The obvious way to do it is to have
axioms 
. We can do it with by
writing the axioms 
, which
comes to n-1 axioms. We then write 
and 
. This ordering trick permits
proving that the 
s are all distinct. The transitivity of <
lets us infer the n(n-1) inequalities we want. Notice that the
ordering has no relation to any properties of of the s, and any
of the n! total orderings of 
will do.
It might be considered more elegant to write functions from the
s to the integers and use the transitivity, etc. of the integers
to infer the inequalities. Thus we would write 
, which comes to n equations.
The index functions are arbitrary, because all they have to do is
assign different indexes to different objects.
Within a computer program, we may give the objects names, e.g. write equations name(Fido) = "Fido", etc. and rely on the computer to assert that the strings "Fido", "Rover", etc. are distinct.
When we have only a few objects, it isn't too much trouble to write the inequalities directly.