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