for S being OrderSortedSign
for w1, w2, w3 being Element of the carrier of S * st w1 <= w2 & w2 <= w3 holds
w1 <= w3