no goals
α : Type u_1
inst✝ : LinearOrder α
s✝ t✝ : Set α
x✝ y z : α
s t : Set α
x : α
⊢ ordConnectedComponent (s ∩ t) x = ordConnectedComponent s x ∩ ordConnectedComponent t x
simp [ordConnectedComponent, setOf_and]