:: deftheorem Def4 defines OSCl OSALG_2:def 4 :
for S1 being OrderSortedSign
for M being ManySortedSet of the carrier of S1
for b₃ being OrderSortedSet of S1 holds
( b₃ = OSCl M iff for s being SortSymbol of S1 holds b₃ . s = union { (M . s1) where s1 is SortSymbol of S1 : s1 <= s } );