ι : Type ?u.185526
α : Type u_1
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
ha : a₂ ≤ a₁ ∧ a₁ ≤ b₂
hb : a₂ ≤ b₁ ∧ b₁ ≤ b₂
⊢ [[a₁, b₁]] ⊆ Icc a₂ b₂
ι : Type ?u.185526
α : Type u_1
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
ha : a₁ ∈ Icc a₂ b₂
hb : b₁ ∈ Icc a₂ b₂
⊢ [[a₁, b₁]] ⊆ Icc a₂ b₂
rw [mem_Icc] at ha hb
no goals
ι : Type ?u.185526
α : Type u_1
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a a₁ a₂ b b₁ b₂ c x : α
ha : a₂ ≤ a₁ ∧ a₁ ≤ b₂
hb : a₂ ≤ b₁ ∧ b₁ ≤ b₂
⊢ [[a₁, b₁]] ⊆ Icc a₂ b₂
exact Icc_subset_Icc (_root_.le_inf ha.1 hb.1) (_root_.sup_le ha.2 hb.2)