α✝ : Type ?u.6443
β : Type ?u.6446
inst✝² : Preorder α✝
inst✝¹ : Preorder β
s t : Set α✝
α : Type u_1
inst✝ : PartialOrder α
a : α
⊢ OrdConnected (Icc a a)
α✝ : Type ?u.6443
β : Type ?u.6446
inst✝² : Preorder α✝
inst✝¹ : Preorder β
s t : Set α✝
α : Type u_1
inst✝ : PartialOrder α
a : α
⊢ OrdConnected {a}
rw [← Icc_self]
no goals
α✝ : Type ?u.6443
β : Type ?u.6446
inst✝² : Preorder α✝
inst✝¹ : Preorder β
s t : Set α✝
α : Type u_1
inst✝ : PartialOrder α
a : α
⊢ OrdConnected (Icc a a)
exact ordConnected_Icc