Description: A closed interval [ A , B ] is closed. (Contributed by Mario Carneiro, 3-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ordttopon.3 | |
|
Assertion | ordtcld3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ordttopon.3 | |
|
2 | inrab | |
|
3 | 1 | ordtcld2 | |
4 | 3 | 3adant3 | |
5 | 1 | ordtcld1 | |
6 | incld | |
|
7 | 4 5 6 | 3imp3i2an | |
8 | 2 7 | eqeltrrid | |