theorem Th37: :: OSALG_2:37

for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1
for U1 being OSSubAlgebra of U0
for A, B being OSSubset of U0 st B = A (\/) the Sorts of U1 holds
(GenOSAlg A) "\/"_os U1 = GenOSAlg B