theorem Set.mem_of_subset_of_mem
theorem Set.mem_of_subset_of_mem: ∀ {α : Type u} {s₁ s₂ : Set α} {a : α}, s₁ ⊆ s₂ → a ∈ s₁ → a ∈ s₂
theorem Set.mem_of_subset_of_mem
theorem Set.mem_of_subset_of_mem: ∀ {α : Type u} {s₁ s₂ : Set α} {a : α}, s₁ ⊆ s₂ → a ∈ s₁ → a ∈ s₂