English
If two subsets s and t are OrdConnected, then their intersection s ∩ t is OrdConnected.
Русский
Если подмножества s и t являются OrdConnected, то их пересечение s ∩ t также OrdConnected.
LaTeX
$$$\operatorname{OrdConnected}(s) \land \operatorname{OrdConnected}(t) \Rightarrow \operatorname{OrdConnected}(s \cap t)$$$
Lean4
theorem inter {s t : Set α} (hs : OrdConnected s) (ht : OrdConnected t) : OrdConnected (s ∩ t) :=
⟨fun _ hx _ hy => subset_inter (hs.out hx.1 hy.1) (ht.out hx.2 hy.2)⟩