apply Set.eq_of_subset_of_subset
α : Type
L : Language α
⊢ kleene_closure α L = {[]} ∪ concat L (kleene_closure α L)
case a
α : Type
L : Language α
⊢ kleene_closure α L ⊆ {[]} ∪ concat L (kleene_closure α L)

case a
α : Type
L : Language α
⊢ {[]} ∪ concat L (kleene_closure α L) ⊆ kleene_closure α L