:: deftheorem Def15 defines UniAlg_join UNIALG_2:def 15 :
for U0 being Universal_Algebra
for b₂ being BinOp of (Sub U0) holds
( b₂ = UniAlg_join U0 iff for x, y being Element of Sub U0
for U1, U2 being strict SubAlgebra of U0 st x = U1 & y = U2 holds
b₂ . (x,y) = U1 "\/" U2 );