Theory Superposition_Calculus.Relation_Extra

theory Relation_Extra
  imports Main
begin

lemma partition_set_around_element:
  assumes tot: "totalp_on N R" and x_in: "x ∈ N"
  shows "N = {y ∈ N. R y x} ∪ {x} ∪ {y ∈ N. R x y}"
proof (intro Set.equalityI Set.subsetI)
  fix z assume "z ∈ N"
  hence "R z x ∨ z = x ∨ R x z"
    using tot[THEN totalp_onD] x_in by auto
  thus "z ∈ {y ∈ N. R y x} ∪ {x} ∪ {y ∈ N. R x y}"
    using ‹z ∈ N› by auto
next
  fix z assume "z ∈ {y ∈ N. R y x} ∪ {x} ∪ {y ∈ N. R x y}"
  hence "z ∈ N ∨ z = x"
    by auto
  thus "z ∈ N"
    using x_in by auto
qed

end