for S being OrderSortedSign
for X being OrderSortedSet of S holds OSCl X = X