Yes! Note that the claim that S is a subset of T is conventionally written in logic as

all e: univ | e in S implies e in T

which becomes vacuously true when S is empty. This treatment of partial functions and empty sets is one of Alloy’s key innovations, and it avoids the nastiness of undefined values that complicated many languages before Alloy.

For those not familiar with that whole rats nest, consider that the formula

some p: Person | p.dog = Rex

becomes undefined in most standard logics if there is any person who doesn’t have a dog, even if Rex is Alice’s dog!

A downside of this is indeed that you need to sometimes strengthen a constraint if you don’t want to subsume the empty case. In an early version of Alloy there was a special operator that you could use to say S is a non-empty subset of T, but I can’t remember what it was. It was a bad idea anyway :-).