How to derive the `one` multiplicity constraint using the Alloy Kernel language?

Question

I was reading Appendix C: Kernel Semantics of the Software Abstraction book (by Daniel Jackson, second edition, very nice read btw!) and found myself a bit stuck in understanding how to derive the one multiplicity constraint using the other kernel constructs.

I understand that no can be derived using expr = none, and some can be derived using the negation of the previous rule but I don't understand how to express the one (and thus lone) constraint using only the kernel constructs (or derivations).

I am probably missing something obvious but I don't see it :)

Answer 1

Here is how I'd express one expr

//there is some expr
not (expr = none)
//and all expr should be one and the same because there's only one expr. 
all x1,x2: expr | x1=x2