for U0 being Universal_Algebra holds UniAlg_join U0 is commutative