simp
case h.left

⊢ 2 ∈ {z | z ≠ 1 ∧ 0 < z.re}

case h.right

⊢ ∀ {y : ℂ}, y ∈ {z | z ≠ 1 ∧ 0 < z.re} → JoinedIn {z | z ≠ 1 ∧ 0 < z.re} 2 y
case h.right

⊢ ∀ {y : ℂ}, y ∈ {z | z ≠ 1 ∧ 0 < z.re} → JoinedIn {z | z ≠ 1 ∧ 0 < z.re} 2 y