:: deftheorem Def21 defines MSAlg_meet MSUALG_2:def 21 :
for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for b₃ being BinOp of (MSSub U0) holds
( b₃ = MSAlg_meet U0 iff for x, y being Element of MSSub U0
for U1, U2 being strict MSSubAlgebra of U0 st x = U1 & y = U2 holds
b₃ . (x,y) = U1 /\ U2 );