:: deftheorem Def13 defines "\/"_os OSALG_2:def 13 :
for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1
for U1, U2 being OSSubAlgebra of U0
for b₅ being strict OSSubAlgebra of U0 holds
( b₅ = U1 "\/"_os U2 iff for A being OSSubset of U0 st A = the Sorts of U1 (\/) the Sorts of U2 holds
b₅ = GenOSAlg A );