intro hs ht x
α : Sort u_1
s t u s₁ s₂ t₁ t₂ : Set α
⊢ s₁.Subset s₂ → t₁.Subset t₂ → (s₁.union t₁).Subset (s₂.union t₂)
α : Sort u_1
s t u s₁ s₂ t₁ t₂ : Set α
hs : s₁.Subset s₂
ht : t₁.Subset t₂
x : α
⊢ x ∈ s₁.union t₁ → x ∈ s₂.union t₂