Description: The positive reals are a subset of the reals. (Contributed by NM, 24-Feb-2008)
Ref | Expression | ||
---|---|---|---|
Assertion | rpssre | $${\u22a2}{\mathbb{R}}^{+}\subseteq \mathbb{R}$$ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rp | $${\u22a2}{\mathbb{R}}^{+}=\left\{{x}\in \mathbb{R}|0<{x}\right\}$$ | |
2 | 1 | ssrab3 | $${\u22a2}{\mathbb{R}}^{+}\subseteq \mathbb{R}$$ |