simpa using Ioc_subset_Icc_self
x✝¹ σ σ'✝ σ''✝ T x : ℝ
xpos : 0 < x
σ' σ'' : ℝ
x✝ : (𝓟 (Ι σ' σ'')).NeBot
this : (atBot ⊔ atTop).NeBot
⊢ 𝓟 (Ι σ' σ'') ×ˢ (atBot ⊔ atTop) ≤ 𝓟 [[σ', σ'']] ×ˢ (atBot ⊔ atTop)
no goals