:: deftheorem Def13 defines "\/" UNIALG_2:def 13 :
for U0 being Universal_Algebra
for U1, U2 being SubAlgebra of U0
for b₄ being strict SubAlgebra of U0 holds
( b₄ = U1 "\/" U2 iff for A being non empty Subset of U0 st A = the carrier of U1 \/ the carrier of U2 holds
b₄ = GenUnivAlg A );