for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for B being MSSubset of U0 holds
( B in SubSort U0 iff B is opers_closed )