theorem Th26: :: UNIALG_2:26

for U0 being with_const_op Universal_Algebra holds UniAlg_meet U0 is commutative