case h
α : Type u_1
β : Type ?u.17119
inst✝ : PartialOrder α
a b c✝ : α
h : a ⩿ b
c : α
⊢ c ∈ Icc a b ↔ c ∈ {a, b}
α : Type u_1
β : Type ?u.17119
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
⊢ Icc a b = {a, b}
ext c
no goals
case h
α : Type u_1
β : Type ?u.17119
inst✝ : PartialOrder α
a b c✝ : α
h : a ⩿ b
c : α
⊢ c ∈ Icc a b ↔ c ∈ {a, b}
exact h.le_and_le_iff