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