Theorem ioossicc

Description: An open interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007)

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

Proof

Step	Hyp	Ref	Expression
1		df-ioo	$$⊢\left(.\right)=\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼\left\{z\in {ℝ}^{*}|\left(x<z\wedge z<y\right)\right\}\right)$$
2		df-icc	$$⊢\left[.\right]=\left(x\in {ℝ}^{*},y\in {ℝ}^{*}⟼\left\{z\in {ℝ}^{*}|\left(x\le z\wedge z\le y\right)\right\}\right)$$
3		xrltle	$$⊢\left(A\in {ℝ}^{*}\wedge w\in {ℝ}^{*}\right)\to \left(A<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]$$