exact ⟨rectangleBorder_subset_rectangle z w, disjoint_singleton_right.mpr pNotOnBorder⟩
z✝ w✝ : ℂ
c : ℝ
z w p : ℂ
pNotOnBorder : p ∉ RectangleBorder z w
⊢ RectangleBorder z w ⊆ Rectangle z w ∧ Disjoint (RectangleBorder z w) {p}
no goals