English
A belongs to the unordered interval between b and c if and only if either b < a ≤ c with a between, or c < a ≤ b with a between.
Русский
Элемент a принадлежит неупорядоченному интервалу между b и c тогда и только тогда, когда либо b < a ≤ c, либо c < a ≤ b.
LaTeX
$$$ a \\in Ι(b,c) \\iff (b < a \\land a \\le c) \\lor (c < a \\land a \\le b) $$$
Lean4
theorem mem_uIoc : a ∈ Ι b c ↔ b < a ∧ a ≤ c ∨ c < a ∧ a ≤ b := by rw [uIoc_eq_union, mem_union, mem_Ioc, mem_Ioc]