Z-Specification = Routes
If you say

$\forall x, x': ran\  routes . x&lt;&gt;x'$

You're only saying that the sequences are different.  For example 

$&lt;London, Berlin, Paris&gt;$ would be different to $&lt;London, Paris, Berlin&gt;$

Instead, you need two quantifiers

$\forall x: ran\  routes . \#x&gt;20$

and

$\forall p,p': Place • p \in ran\ (ran\ routes) \land p' \in ran\ (ran\ routes)  \implies p&lt;&gt;p'$

One for the length as you had and one for the condition that all elements must be unique.  Note the double $ran$ expression since a sequence is defined as a function between its indexes and its values (the range).