Description: A T_1 space is a topological space. (Contributed by Jeff Hankins, 1-Feb-2010)
Ref | Expression | ||
---|---|---|---|
Assertion | t1top | |- ( J e. Fre -> J e. Top ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | |- U. J = U. J |
|
2 | 1 | ist1 | |- ( J e. Fre <-> ( J e. Top /\ A. x e. U. J { x } e. ( Clsd ` J ) ) ) |
3 | 2 | simplbi | |- ( J e. Fre -> J e. Top ) |