theorem Th42: :: OSALG_2:42

for S1 being OrderSortedSign
for OU0 being OSAlgebra of S1 holds OSSub OU0 c= MSSub OU0