:: deftheorem Def18 defines "\/" MSUALG_2:def 18 :
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for U1, U2 being MSSubAlgebra of U0
for b₅ being strict MSSubAlgebra of U0 holds
( b₅ = U1 "\/" U2 iff for A being MSSubset of U0 st A = the Sorts of U1 (\/) the Sorts of U2 holds
b₅ = GenMSAlg A );