exact hL₀ h
case basic
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 x✝ : V
h : x✝ ∈ S
⊢ x✝ ∈ L
no goals