I think this model is semantically symmetrical in both sets
If you are convinced that the model of the spec is symmetrical, then
you should be able to prove that it satisfies the definition of
symmetry.
Thank you for making me realize that symmetry with respect to a set S
can be broken by CHOOSE expressions involving S other than ones of the
form CHOOSE x \in S : ... -- for example a CHOOSE _expression_ like
Map == CHOOSE f \in [S -> T] : ...
As I did mention, symmetry can also be broken by instantiating a
constant like Map with an _expression_ that explicitly mentions
individual elements of S.
Leslie