for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A, B being MSSubset of U0 holds
( B in SubSort A iff ( B is opers_closed & Constants U0 c= B & A c= B ) )