Thm* L,M,N:LangOver(Alph). (L (M U N)) = ((L M) U (L N)) lang_inters_union

Thm* L,M,N:LangOver(Alph). (L U (M N)) = ((L U M) (L U N)) lang_union_inters

Thm* L,M,N:LangOver(Alph). (L U (M U N)) = ((L U M) U N) lang_union_assoc

Thm* L,M:LangOver(Alph). (L U M) = (M U L) lang_union_commut

Thm* L:LangOver(Alph). (L U L) = L lang_union_idemp

Thm* L,L',M,M':LangOver(Alph). L = L' M = M' (L U M) = (L' U M') lang_union_functionality