Metamath Proof Explorer


Theorem sshaus

Description: A topology finer than a Hausdorff topology is Hausdorff. (Contributed by Mario Carneiro, 2-Mar-2015)

Ref Expression
Hypothesis t1sep.1 X=J
Assertion sshaus JHausKTopOnXJKKHaus

Proof

Step Hyp Ref Expression
1 t1sep.1 X=J
2 haustop JHausJTop
3 cnhaus JHausIX:X1-1XIXKCnJKHaus
4 1 2 3 sshauslem JHausKTopOnXJKKHaus