Description: A closed-above, open-below interval is a subset of its closure. (Contributed by Thierry Arnoux, 1-Apr-2017)
Ref | Expression | ||
---|---|---|---|
Assertion | iocssicc | |- ( A (,] B ) C_ ( A [,] B ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ioc | |- (,] = ( a e. RR* , b e. RR* |-> { x e. RR* | ( a < x /\ x <_ b ) } ) |
|
2 | df-icc | |- [,] = ( a e. RR* , b e. RR* |-> { x e. RR* | ( a <_ x /\ x <_ b ) } ) |
|
3 | xrltle | |- ( ( A e. RR* /\ w e. RR* ) -> ( A < w -> A <_ w ) ) |
|
4 | idd | |- ( ( w e. RR* /\ B e. RR* ) -> ( w <_ B -> w <_ B ) ) |
|
5 | 1 2 3 4 | ixxssixx | |- ( A (,] B ) C_ ( A [,] B ) |