Theorem iocssicc

Description: A closed-above, open-below interval is a subset of its closure. (Contributed by Thierry Arnoux, 1-Apr-2017)

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

Proof

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