simp_rw [RectangleBorder, Set.mem_union, not_or]
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
h : p.re ≠ z.re ∧ p.re ≠ w.re ∧ p.im ≠ z.im ∧ p.im ≠ w.im
⊢ p ∉ RectangleBorder z w
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
h : p.re ≠ z.re ∧ p.re ≠ w.re ∧ p.im ≠ z.im ∧ p.im ≠ w.im
⊢ ((p ∉ [[z.re, w.re]] ×ℂ {z.im} ∧ p ∉ {z.re} ×ℂ [[z.im, w.im]]) ∧ p ∉ [[z.re, w.re]] ×ℂ {w.im}) ∧
    p ∉ {w.re} ×ℂ [[z.im, w.im]]