English
For all a, b, the closed interval Icc(a,b) is bounded below with respect to >; lower bound by a (exists due to NoMinOrder).
Русский
Для всех a, b замкнутый интервал Icc(a,b) ограничен снизу относительно >; нижняя граница — a (существует из NoMinOrder).
LaTeX
$$$\forall a,b:\ Bound\ (>)(Icc\ a\ b)$$$
Lean4
theorem bounded_gt_Icc [Preorder α] [NoMinOrder α] (a b : α) : Bounded (· > ·) (Icc a b) :=
(bounded_gt_Ici a).mono Set.Icc_subset_Ici_self