begin
Lm0:
for Z being open Subset of REAL st 0 in Z holds
(id Z) " {0 } = {0 }
Lm1:
right_open_halfline 0 = { g where g is Real : 0 < g }
by XXREAL_1:230;
A:
( - 1 is Real & - (1 / 2) is Real & 1 / 2 is Real )
by XREAL_0:def 1;
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th1:
theorem
theorem Th2:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th3:
theorem
theorem
theorem
theorem Th4:
theorem
theorem
theorem
theorem Th5:
theorem
theorem
theorem Th6:
theorem
theorem
theorem
theorem
theorem
theorem Th7:
theorem
theorem
theorem
theorem Th8:
theorem
theorem
theorem
theorem
theorem
theorem Th9:
theorem
theorem
theorem
theorem Th10:
theorem Th11:
theorem
theorem