:: deftheorem Def5 defines meet UNIALG_3:def 5 :
for U0 being strict with_const_op Universal_Algebra
for H being non empty Subset of (Sub U0)
for b₃ being strict SubAlgebra of U0 holds
( b₃ = meet H iff the carrier of b₃ = meet ((Carr U0) .: H) );