Metamath Proof Explorer


Theorem retop

Description: The standard topology on the reals. (Contributed by FL, 4-Jun-2007)

Ref Expression
Assertion retop topGenran.Top

Proof

Step Hyp Ref Expression
1 retopbas ran.TopBases
2 tgcl ran.TopBasestopGenran.Top
3 1 2 ax-mp topGenran.Top