theorem Th5: :: OSALG_2:5

for S being OrderSortedSign
for U0 being OSAlgebra of S
for U1 being MSAlgebra over S holds
( U1 is OSSubAlgebra of U0 iff ( the Sorts of U1 is OSSubset of U0 & ( for B being OSSubset of U0 st B = the Sorts of U1 holds
( B is opers_closed & the Charact of U1 = Opers (U0,B) ) ) ) )