∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e : OpenPartialHomeomorph X Y} {s : Set X} {t : Set Y} {x : X}, e.IsImage s t → x ∈ e.source → (↑e x ∈ t ↔ x ∈ s)