Description: A Hausdorff space is a topology. (Contributed by NM, 5-Mar-2007)
Ref | Expression | ||
---|---|---|---|
Assertion | haustop | |- ( J e. Haus -> J e. Top ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid | |- U. J = U. J |
|
2 | 1 | ishaus | |- ( J e. Haus <-> ( J e. Top /\ A. x e. U. J A. y e. U. J ( x =/= y -> E. n e. J E. m e. J ( x e. n /\ y e. m /\ ( n i^i m ) = (/) ) ) ) ) |
3 | 2 | simplbi | |- ( J e. Haus -> J e. Top ) |