Theorem fzossfz

Description: A half-open range is contained in the corresponding closed range. (Contributed by Stefan O'Rear, 23-Aug-2015) (Revised by Mario Carneiro, 29-Sep-2015)

	Ref	Expression
Assertion	fzossfz	$$⊢\left(A..^B\right)\subseteq \left(A\dots B\right)$$

Proof

Step	Hyp	Ref	Expression
1		elfzofz	$$⊢x\in \left(A..^B\right)\to x\in \left(A\dots B\right)$$
2	1	ssriv	$$⊢\left(A..^B\right)\subseteq \left(A\dots B\right)$$