# How to define an invariant that describes a sorted sequence

Hi,
I'm trying to define an invariant that specfies a sequence should be (strictly) ordered, and am not getting the correct syntax. My sequence is called myList and the invariant is called Ordered

define
Ordered == \A i \in 1..Len(myList), j \in 1..Len(myList), i < j: myList[i] < myList[j]
end define;

Thanks,
Pramod