Set_is_Subset_of_Itself
Provedproofwikisubsets
Every set is a subset of itself Thus, by definition, the relation '''is a subset of''' is reflexive.
Preamble
import Mathlib.Data.Set.Basic
Formal statement
theorem Set_is_Subset_of_Itself {α : Type*} (S : Set α) : S ⊆ S := by sorrySource