no goals
X : Type u_1
Y : Type ?u.615739
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y z : X
ι : Type ?u.615754
F : Set X
⊢ JoinedIn univ x y ↔ Joined x y
simp [JoinedIn, Joined, exists_true_iff_nonempty]