begin
X:
- 1 is Real
by XREAL_0:def 1;
theorem Th1:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
Lm1:
right_open_halfline 0 = { g where g is Real : 0 < g }
by XXREAL_1:230;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem