Set_Difference_with_Self_is_Empty_Set
Provedempty-setproofwikiset-difference
Set Difference with Self is Empty Set
Preamble
import Mathlib.Data.Set.Basic
Formal statement
theorem Set_Difference_with_Self_is_Empty_Set {α : Type _} (S : Set α) : S \ S = ∅ := by sorry