:: deftheorem Def11 defines OSMSubSort OSALG_2:def 11 :
for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1
for A, b₄ being OSSubset of OU0 holds
( b₄ = OSMSubSort A iff for s being SortSymbol of S1 holds b₄ . s = meet (OSSubSort (A,s)) );