obtain ⟨y, hyA, hyB⟩ := nonempty_of_ssubset ⟨hAB.1, hBA⟩
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x✝ : E
hAB : IsExtreme 𝕜 s t
hBA : ¬s ⊆ t
x : E
hxB : x ∈ t
⊢ x ∈ frontier s
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : NormedLinearOrderedField 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s t : Set E
x✝ : E
hAB : IsExtreme 𝕜 s t
hBA : ¬s ⊆ t
x : E
hxB : x ∈ t
y : E
hyA : y ∈ s
hyB : y ∉ t
⊢ x ∈ frontier s