theorem :: OSALG_2:9

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