Z-Specification = Routes


enter image description here

Im trying to make an invariant for this Z schema about routes.

1) The invariant should express that each route should contain at least 20 different places. First of all i thought of doing a universal quantification such as:

∀x : ran routes • ( #x>20 ∧ x ≠ x’)

However i’m really not sure if thats correct that implying 20 different places.