:: deftheorem Def16 defines UniAlg_meet UNIALG_2:def 16 :
for U0 being Universal_Algebra
for b₂ being BinOp of (Sub U0) holds
( b₂ = UniAlg_meet 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 );