Description: The closure of a closed set is itself. (Contributed by Stefan O'Rear, 31-Jan-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | mrcfval.f | |
|
Assertion | mrcid | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mrcfval.f | |
|
2 | mress | |
|
3 | 1 | mrcval | |
4 | 2 3 | syldan | |
5 | intmin | |
|
6 | 5 | adantl | |
7 | 4 6 | eqtrd | |