theorem Th3: :: MSUALG_2:3

for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for B being MSSubset of U0 st B = the Sorts of U0 holds
( B is opers_closed & ( for o being OperSymbol of S holds o /. B = Den (o,U0) ) )