Description: The topology extractor on a topological space is a topology. (Contributed by FL, 27-Jun-2014)
Ref | Expression | ||
---|---|---|---|
Hypothesis | tpstop.j | |
|
Assertion | tpstop | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tpstop.j | |
|
2 | eqid | |
|
3 | 2 1 | istps2 | |
4 | 3 | simplbi | |