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 | |- ( A ..^ B ) C_ ( A ... B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elfzofz | |- ( x e. ( A ..^ B ) -> x e. ( A ... B ) ) |
|
| 2 | 1 | ssriv | |- ( A ..^ B ) C_ ( A ... B ) |