Metamath Proof Explorer

Theorem tdrgtps

Description: A topological division ring is a topological space. (Contributed by Mario Carneiro, 5-Oct-2015)

		Ref	Expression
	Assertion	tdrgtps	$⊢ R \in TopDRing \to R \in TopSp$

Step	Hyp	Ref	Expression
1		tdrgtrg	$⊢ R \in TopDRing \to R \in TopRing$
2		trgtps	$⊢ R \in TopRing \to R \in TopSp$
3	1 2	syl	$⊢ R \in TopDRing \to R \in TopSp$