Metamath Proof Explorer


Theorem tlmtps

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

Ref Expression
Assertion tlmtps WTopModWTopSp

Proof

Step Hyp Ref Expression
1 tlmtmd WTopModWTopMnd
2 tmdtps WTopMndWTopSp
3 1 2 syl WTopModWTopSp