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	⊢ ( 𝐴 ..^ 𝐵 ) ⊆ ( 𝐴 ... 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		elfzofz	⊢ ( 𝑥 ∈ ( 𝐴 ..^ 𝐵 ) → 𝑥 ∈ ( 𝐴 ... 𝐵 ) )
2	1	ssriv	⊢ ( 𝐴 ..^ 𝐵 ) ⊆ ( 𝐴 ... 𝐵 )