Theorem qtopbas

Description: The set of open intervals with rational endpoints forms a basis for a topology. (Contributed by NM, 8-Mar-2007)

	Ref	Expression
Assertion	qtopbas	$$⊢\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\in \mathrm{TopBases}$$

Proof

Step	Hyp	Ref	Expression
1		qssre	$$⊢\mathbb{Q}\subseteq ℝ$$
2		ressxr	$$⊢ℝ\subseteq {ℝ}^{*}$$
3	1 2	sstri	$$⊢\mathbb{Q}\subseteq {ℝ}^{*}$$
4	3	qtopbaslem	$$⊢\left(.\right)\left[\mathbb{Q}\times \mathbb{Q}\right]\in \mathrm{TopBases}$$