:: deftheorem Def15 defines OSAlg_join OSALG_2:def 15 :
for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1
for b₃ being BinOp of (OSSub U0) holds
( b₃ = OSAlg_join U0 iff for x, y being Element of OSSub U0
for U1, U2 being strict OSSubAlgebra of U0 st x = U1 & y = U2 holds
b₃ . (x,y) = U1 "\/"_os U2 );