   Several things are notable about this axiom and its formulation. It is in the form of a universally quantified equivalence, with the right-hand side as it were explicating the left-hand side, so that it is a kind of implicit definition of the primitive ‘\(\isa\)’. The right-hand side, taking its cue from Russell, says that there is at least one \(A\) (first conjunct), there is at most one \(A\) (second conjunct), and any \(A\) is an \(a\) (third conjunct). The use of capital letter variables is an informal aid to perspicuity: they mark the positions in sentences (especially before ‘\(\isa\)’) where a variable can only yield a truth of its immediate context if it is singular. Where small Italic variables are used, there is no such presumption of singularity. In principle only one typeface of variables is needed. On the basis of his axiom and several rules of inference, Leśniewski developed a powerful system of general logic comparable in strength to a simple type theory: he writes in 1929, “In 1921 I developed my ‘theory of types’ […] It was something like Whitehead’s and Russell’s theory of types, which I had generalised and simplified in a certain way” (Collected Works, 421). 