for U0 being with_const_op Universal_Algebra
for H being non empty Subset of (Sub U0) holds meet ((Carr U0) .: H) is non empty Subset of U0