Theorem icossicc

Description: A closed-below, open-above interval is a subset of its closure. (Contributed by Thierry Arnoux, 25-Oct-2016)

	Ref	Expression
Assertion	icossicc	$$⊢\left[A,B\right)\subseteq \left[A,B\right]$$

Proof

Step	Hyp	Ref	Expression
1		df-ico	$$⊢\left[.\right)=\left(a\in {ℝ}^{*},b\in {ℝ}^{*}⟼\left\{x\in {ℝ}^{*}|\left(a\le x\wedge x<b\right)\right\}\right)$$
2		df-icc	$$⊢\left[.\right]=\left(a\in {ℝ}^{*},b\in {ℝ}^{*}⟼\left\{x\in {ℝ}^{*}|\left(a\le x\wedge x\le b\right)\right\}\right)$$
3		idd	$$⊢\left(A\in {ℝ}^{*}\wedge w\in {ℝ}^{*}\right)\to \left(A\le w\to A\le w\right)$$
4		xrltle	$$⊢\left(w\in {ℝ}^{*}\wedge B\in {ℝ}^{*}\right)\to \left(w<B\to w\le B\right)$$
5	1 2 3 4	ixxssixx	$$⊢\left[A,B\right)\subseteq \left[A,B\right]$$