Theorem: LO.FirstOrder.ModelsTheory.of_add_right (Logic/FirstOrder/Completeness/Lemmata.lean)

State before:
L : Language
M : Type w
inst✝² : Nonempty M
inst✝¹ : Structure L M
T U V : Theory L
inst✝ : M ⊧ₘ* T + U
⊢ U ⊆ T + U
Tactic:
simp [Theory.add_def]
State after:
no goals