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 (M N)) = ((L M) N) lang_inters_assoc

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

Thm* L:LangOver(Alph). (L L) = L lang_inters_idemp

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

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