:: deftheorem Def16 defines OSAlg_meet OSALG_2:def 16 :
for S1 being OrderSortedSign
for U0 being non-empty OSAlgebra of S1
for b₃ being BinOp of (OSSub U0) holds
( b₃ = OSAlg_meet 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 /\ U2 );