theorem Th27: :: UNIALG_2:27

for U0 being with_const_op Universal_Algebra holds UniAlg_meet U0 is associative