intro x hx
V : Type u_1
inst✝ : MetricSpace V
u v w : V
S L : Set V
hL₀ : S ⊆ L
out_closed : ∀ {x y z : V}, x ∈ L → y ∈ L → sbtw x y z → z ∈ L
in_closed : ∀ {x y z : V}, x ∈ L → y ∈ L → sbtw x z y → z ∈ L
⊢ GenerateLine S ⊆ L
V : Type u_1
inst✝ : MetricSpace V
u v w : V
S L : Set V
hL₀ : S ⊆ L
out_closed : ∀ {x y z : V}, x ∈ L → y ∈ L → sbtw x y z → z ∈ L
in_closed : ∀ {x y z : V}, x ∈ L → y ∈ L → sbtw x z y → z ∈ L
x : V
hx : x ∈ GenerateLine S
⊢ x ∈ L