Theorem retop

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

	Ref	Expression
Assertion	retop	⊢ ( topGen ‘ ran (,) ) ∈ Top

Proof

Step	Hyp	Ref	Expression
1		retopbas	⊢ ran (,) ∈ TopBases
2		tgcl	⊢ ( ran (,) ∈ TopBases → ( topGen ‘ ran (,) ) ∈ Top )
3	1 2	ax-mp	⊢ ( topGen ‘ ran (,) ) ∈ Top