Description: An open interval is a subset of its closure. (Contributed by Paul Chapman, 18-Oct-2007)
Ref | Expression | ||
---|---|---|---|
Assertion | ioossicc | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ioo | |
|
2 | df-icc | |
|
3 | xrltle | |
|
4 | xrltle | |
|
5 | 1 2 3 4 | ixxssixx | |