:: INT_1 semantic presentation

REAL is non empty V33() set

K99() is set
bool K99() is set
bool (bool K99()) is set
DEDEKIND_CUTS is Element of bool (bool K99())
REAL+ is set
COMPLEX is non empty V33() set

{} is set
is set

is set
is set
is set
is set
() \ is Element of bool ()
bool () is set
INT is non empty V33() set

() \ is Element of bool ()
bool () is set
K105() is Element of K99()
is set

[0,0] is set
{0,0} is set
is set
is set

r is set

b is set
j9 is set
[b,j9] is set
{b,j9} is set
{b} is set
{{b,j9},{b}} is set
a is ext-real V31() real Element of REAL

+ (a,09) is ext-real V31() real Element of REAL
c6 is Element of REAL+
[0,c6] is set
{0,c6} is set
{{0,c6},} is set
i9 is Element of REAL+
i9 - c6 is set
- 09 is ext-real non positive V31() real Element of REAL
a + 09 is ext-real V31() real Element of REAL
x9 is ext-real V31() real Element of REAL
y9 is ext-real V31() real Element of REAL
[*x9,y9*] is Element of COMPLEX
y1 is ext-real V31() real Element of REAL
y2 is ext-real V31() real Element of REAL
[*y1,y2*] is Element of COMPLEX
+ (x9,y1) is ext-real V31() real Element of REAL
+ (y9,y2) is ext-real V31() real Element of REAL
[*(+ (x9,y1)),(+ (y9,y2))*] is Element of COMPLEX
r is set

- a is ext-real non positive V31() real Element of REAL
b is ext-real V31() real Element of REAL
b + a is ext-real V31() real Element of REAL
j9 is ext-real V31() real Element of REAL
09 is ext-real V31() real Element of REAL
[*j9,09*] is Element of COMPLEX
c6 is ext-real V31() real Element of REAL
i9 is ext-real V31() real Element of REAL
[*c6,i9*] is Element of COMPLEX
+ (j9,c6) is ext-real V31() real Element of REAL
+ (09,i9) is ext-real V31() real Element of REAL
[*(+ (j9,c6)),(+ (09,i9))*] is Element of COMPLEX
x9 is Element of REAL+
y9 is Element of REAL+
x9 + y9 is Element of REAL+

x9 is Element of REAL+
[0,x9] is set
{0,x9} is set
{{0,x9},} is set
y9 is Element of REAL+
y9 - x9 is set
r is set
a is set

- b is ext-real non positive V31() real Element of REAL

a is set

- b is ext-real non positive V31() real Element of REAL

a is set

- j9 is ext-real non positive V31() real Element of REAL
r is Element of INT
r is ext-real V31() real set

- a is ext-real non positive V31() real set
r is ext-real V31() real set
r is set
r is set
r is set
a is ext-real V31() real Element of REAL
r is ext-real V31() real () set
a is ext-real V31() real () set
r + a is ext-real V31() real set

- b is ext-real non positive V31() real Element of REAL

- j9 is ext-real non positive V31() real Element of REAL
b - j9 is ext-real V31() real Element of REAL

- 09 is ext-real non positive V31() real set
(- j9) + b is ext-real V31() real Element of REAL

j9 - b is ext-real V31() real Element of REAL

- 09 is ext-real non positive V31() real set
(- b) + j9 is ext-real V31() real Element of REAL

- (j9 + b) is ext-real non positive V31() real Element of REAL
r * a is ext-real V31() real set

- b is ext-real non positive V31() real Element of REAL

- j9 is ext-real non positive V31() real Element of REAL

- (j9 * b) is ext-real non positive V31() real Element of REAL
r is ext-real V31() real () set
- r is ext-real V31() real set

- b is ext-real non positive V31() real Element of REAL
r is ext-real V31() real () set
a is ext-real V31() real () set
r - a is ext-real V31() real set
- a is ext-real V31() real () set
r + (- a) is ext-real V31() real () set
r is ext-real V31() real () set

- a is ext-real non positive V31() real () Element of REAL
r is ext-real V31() real set
r + 1 is ext-real V31() real Element of REAL
r - 1 is ext-real V31() real Element of REAL
r is ext-real V31() real () set
a is ext-real V31() real () set
a - r is ext-real V31() real () set
r - r is ext-real V31() real () set

a is ext-real V31() real () set
a + r is ext-real V31() real () Element of REAL
b is ext-real V31() real () set
0 + (a + r) is ext-real V31() real () Element of REAL
r + b is ext-real V31() real () Element of REAL
j9 is ext-real V31() real () set
a + j9 is ext-real V31() real () set
(a + j9) - j9 is ext-real V31() real () set
b + j9 is ext-real V31() real () set
(b + j9) - j9 is ext-real V31() real () set

r is ext-real V31() real () set

r is ext-real V31() real () set
r + 1 is ext-real V31() real () Element of REAL
a is ext-real V31() real () set
- r is ext-real V31() real () set
a + (- r) is ext-real V31() real () set
r + (- r) is ext-real V31() real () set
1 + r is ext-real V31() real () Element of REAL
(a + (- r)) + r is ext-real V31() real () set
- 1 is ext-real non positive V31() real () Element of REAL
r is ext-real V31() real () set
- r is ext-real V31() real () set
- (- r) is ext-real V31() real () set
r is ext-real V31() real () set
a is ext-real V31() real () set
r * a is ext-real V31() real () set
- r is ext-real V31() real () set
- a is ext-real V31() real () set
(- r) * (- a) is ext-real V31() real () set
- (- r) is ext-real V31() real () set
r is ext-real V31() real () set
a is ext-real V31() real () set
r * a is ext-real V31() real () set
- r is ext-real V31() real () set
(- r) * a is ext-real V31() real () set
- (- r) is ext-real V31() real () set
r is ext-real V31() real () set
a is ext-real V31() real () set
a - r is ext-real V31() real () set

r + b is ext-real V31() real () Element of REAL
r is ext-real V31() real () set
a is ext-real V31() real () set
a - r is ext-real V31() real () set

a - b is ext-real V31() real () Element of REAL

r is set
a is set
a is Element of bool INT
b is ext-real V31() real () set
j9 is ext-real V31() real () set
F1() is ext-real V31() real () set

b is ext-real V31() real () set
b - F1() is ext-real V31() real () set
b - 1 is ext-real V31() real () Element of REAL
a is ext-real V31() real () set
a + F1() is ext-real V31() real () set
(b - 1) - F1() is ext-real V31() real () Element of REAL
(b - 1) + 1 is ext-real V31() real () Element of REAL
r is ext-real V31() real () set
r - F1() is ext-real V31() real () set

b is ext-real V31() real () set
b - F1() is ext-real V31() real () set
F1() is ext-real V31() real () set
- F1() is ext-real V31() real () set
r is ext-real V31() real () set
r + 1 is ext-real V31() real () Element of REAL
a is ext-real V31() real () set
- a is ext-real V31() real () set
a + 1 is ext-real V31() real () Element of REAL
- (a + 1) is ext-real V31() real () Element of REAL
(- a) - 1 is ext-real V31() real () Element of REAL
- ((- a) - 1) is ext-real V31() real () Element of REAL
- (- F1()) is ext-real V31() real () set
(a + 1) - 1 is ext-real V31() real () Element of REAL
r is ext-real V31() real () set
- r is ext-real V31() real () set
a is ext-real V31() real () set
- a is ext-real V31() real () set
F1() is ext-real V31() real () set
r is ext-real V31() real () set
a is ext-real V31() real () set
a - 1 is ext-real V31() real () Element of REAL
a is ext-real V31() real () set
a + 1 is ext-real V31() real () Element of REAL
F1() is ext-real V31() real () set
r is ext-real V31() real () set
r is ext-real V31() real () set

F1() + a is ext-real V31() real () Element of REAL

F1() + a is ext-real V31() real () set
b is ext-real V31() real () set
j9 is ext-real V31() real () set
b - F1() is ext-real V31() real () set
j9 - F1() is ext-real V31() real () set

F1() + 09 is ext-real V31() real () Element of REAL
j9 is ext-real V31() real () set
F1() is ext-real V31() real () set
r is ext-real V31() real () set
r is ext-real V31() real () set

F1() - a is ext-real V31() real () Element of REAL

F1() - a is ext-real V31() real () set
b is ext-real V31() real () set
j9 is ext-real V31() real () set

F1() - 09 is ext-real V31() real () Element of REAL
- b is ext-real V31() real () set
F1() + (- b) is ext-real V31() real () set
(F1() + (- b)) - F1() is ext-real V31() real () set
F1() - j9 is ext-real V31() real () set
(F1() - j9) - F1() is ext-real V31() real () set
- j9 is ext-real V31() real () set
F1() + (- j9) is ext-real V31() real () set
(F1() + (- j9)) - F1() is ext-real V31() real () set
j9 is ext-real V31() real () set
b is ext-real V31() real () set
b * 1 is ext-real V31() real () set
r is ext-real V31() real () set
a is ext-real V31() real () set
b is ext-real V31() real () set
r - a is ext-real V31() real () set
j9 is ext-real V31() real () set
b * j9 is ext-real V31() real () set
r is ext-real V31() real () set
a is ext-real V31() real () set
a * 0 is ext-real V31() real () Element of REAL
r - r is ext-real V31() real () set
r is ext-real V31() real () set
r * (- 1) is ext-real V31() real () Element of REAL
0 - r is ext-real V31() real () Element of REAL
r * 1 is ext-real V31() real () Element of REAL
r - 0 is ext-real V31() real () Element of REAL
r is ext-real V31() real () set
a is ext-real V31() real () set
r - a is ext-real V31() real () set
1 * (r - a) is ext-real V31() real () Element of REAL
r is ext-real V31() real () set
a is ext-real V31() real () set
b is ext-real V31() real () set
r - a is ext-real V31() real () set
j9 is ext-real V31() real () set
b * j9 is ext-real V31() real () set
a - r is ext-real V31() real () set
- j9 is ext-real V31() real () set
b * (- j9) is ext-real V31() real () set
r is ext-real V31() real () set
a is ext-real V31() real () set
b is ext-real V31() real () set
j9 is ext-real V31() real () set
r - a is ext-real V31() real () set
09 is ext-real V31() real () set
b * 09 is ext-real V31() real () set
a - j9 is ext-real V31() real () set
c6 is ext-real V31() real () set
b * c6 is ext-real V31() real () set
09 + c6 is ext-real V31() real () set
b * (09 + c6) is ext-real V31() real () set
r - j9 is ext-real V31() real () set
r is ext-real V31() real () set
a is ext-real V31() real () set
b is ext-real V31() real () set
j9 is ext-real V31() real () set
r + j9 is ext-real V31() real () set
09 is ext-real V31() real () set
a + 09 is ext-real V31() real () set
r - a is ext-real V31() real () set
c6 is ext-real V31() real () set
b * c6 is ext-real V31() real () set
j9 - 09 is ext-real V31() real () set
i9 is ext-real V31() real () set
b * i9 is ext-real V31() real () set
c6 + i9 is ext-real V31() real () set
b * (c6 + i9) is ext-real V31() real () set
(r + j9) - (a + 09) is ext-real V31() real () set
r is ext-real V31() real () set
a is ext-real V31() real () set
b is ext-real V31() real () set
j9 is ext-real V31() real () set
r - j9 is ext-real V31() real () set
09 is ext-real V31() real () set
a - 09 is ext-real V31() real () set
r - a is ext-real V31() real () set
c6 is ext-real V31() real () set
b * c6 is ext-real V31() real () set
j9 - 09 is ext-real V31() real () set
i9 is ext-real V31() real () set
b * i9 is ext-real V31() real () set
(r - j9) - (a - 09) is ext-real V31() real () set
c6 - i9 is ext-real V31() real () set
b * (c6 - i9) is ext-real V31() real () set
r is ext-real V31() real () set
a is ext-real V31() real () set
b is ext-real V31() real () set
j9 is ext-real V31() real () set
r * j9 is ext-real V31() real () set
09 is ext-real V31() real () set
a * 09 is ext-real V31() real () set
r - a is ext-real V31() real () set
c6 is ext-real V31() real () set
b * c6 is ext-real V31() real () set
j9 - 09 is ext-real V31() real () set
i9 is ext-real V31() real () set
b * i9 is ext-real V31() real () set
(r * j9) - (a * 09) is ext-real V31() real () set
(r - a) * j9 is ext-real V31() real () set
(j9 - 09) * a is ext-real V31() real () set
((r - a) * j9) + ((j9 - 09) * a) is ext-real V31() real () set
(b * c6) * j9 is ext-real V31() real () set
(b * i9) * a is ext-real V31() real () set
((b * c6) * j9) + ((b * i9) * a) is ext-real V31() real () set
c6 * j9 is ext-real V31() real () set
i9 * a is ext-real V31() real () set
(c6 * j9) + (i9 * a) is ext-real V31() real () set
b * ((c6 * j9) + (i9 * a)) is ext-real V31() real () set
r is ext-real V31() real () set
a is ext-real V31() real () set
r + a is ext-real V31() real () set
b is ext-real V31() real () set
b - a is ext-real V31() real () set
j9 is ext-real V31() real () set
(r + a) - b is ext-real V31() real () set
r - (b - a) is ext-real V31() real () set
09 is ext-real V31() real () set
j9 * 09 is ext-real V31() real () set
r - (b - a) is ext-real V31() real () set
(r + a) - b is ext-real V31() real () set
09 is ext-real V31() real () set
j9 * 09 is ext-real V31() real () set
r is ext-real V31() real () set
a is ext-real V31() real () set
r * a is ext-real V31() real () set
b is ext-real V31() real () set
j9 is ext-real V31() real () set
09 is ext-real V31() real () set
j9 - 09 is ext-real V31() real () set
c6 is ext-real V31() real () set
b * c6 is ext-real V31() real () set
a * c6 is ext-real V31() real () set
r * (a * c6) is ext-real V31() real () set
r is ext-real V31() real () set
a is ext-real V31() real () set
b is ext-real V31() real () set
r + b is ext-real V31() real () set
r - a is ext-real V31() real () set
j9 is ext-real V31() real () set
b * j9 is ext-real V31() real () set
j9 + 1 is ext-real V31() real () Element of REAL
b * (j9 + 1) is ext-real V31() real () Element of REAL
(r + b) - a is ext-real V31() real () set
(r + b) - a is ext-real V31() real () set
j9 is ext-real V31() real () set
b * j9 is ext-real V31() real () set
j9 - 1 is ext-real V31() real () Element of REAL
b * (j9 - 1) is ext-real V31() real () Element of REAL
r - a is ext-real V31() real () set
r is ext-real V31() real () set
a is ext-real V31() real () set
b is ext-real V31() real () set
r - b is ext-real V31() real () set
r - a is ext-real V31() real () set
j9 is ext-real V31() real () set
b * j9 is ext-real V31() real () set
j9 - 1 is ext-real V31() real () Element of REAL
b * (j9 - 1) is ext-real V31() real () Element of REAL
(r - b) - a is ext-real V31() real () set
(r - b) - a is ext-real V31() real () set
j9 is ext-real V31() real () set
b * j9 is ext-real V31() real () set
j9 + 1 is ext-real V31() real () Element of REAL
b * (j9 + 1) is ext-real V31() real () Element of REAL
r - a is ext-real V31() real () set
r is ext-real V31() real set
r - 1 is ext-real V31() real Element of REAL
a is ext-real V31() real () set
b is ext-real V31() real () set
b - a is ext-real V31() real () set
a + (b - a) is ext-real V31() real () set
j9 is ext-real V31() real () set
a + j9 is ext-real V31() real () set
(r - 1) + 1 is ext-real V31() real Element of REAL
r + (- 1) is ext-real V31() real Element of REAL
r is ext-real V31() real set
r + 1 is ext-real V31() real Element of REAL
a is ext-real V31() real () set
b is ext-real V31() real () set
b - a is ext-real V31() real () set
a + (b - a) is ext-real V31() real () set
j9 is ext-real V31() real () set
a + j9 is ext-real V31() real () set
(r + 1) + (- 1) is ext-real V31() real Element of REAL
r is ext-real V31() real set
a is Element of bool REAL
b is ext-real V31() real set
j9 is ext-real V31() real set
b is ext-real V31() real set
b + 0 is ext-real V31() real Element of REAL
b + (- 1) is ext-real V31() real Element of REAL
j9 is ext-real V31() real set
b - 1 is ext-real V31() real Element of REAL
09 is ext-real V31() real set
09 + 1 is ext-real V31() real Element of REAL
(b - 1) + 1 is ext-real V31() real Element of REAL
j9 is ext-real V31() real set

r is ext-real V31() real set
r - 1 is ext-real V31() real Element of REAL
- r is ext-real V31() real set

- (- r) is ext-real V31() real set
- a is ext-real non positive V31() real () Element of REAL
b is ext-real V31() real () set
b + r is ext-real V31() real set
r + (- a) is ext-real V31() real Element of REAL

b is ext-real V31() real () set
b - 1 is ext-real V31() real () Element of REAL
a is ext-real V31() real () set
b is ext-real V31() real () set
a is ext-real V31() real () set
b is ext-real V31() real set
b - 1 is ext-real V31() real Element of REAL
a - 1 is ext-real V31() real () Element of REAL
r is ext-real V31() real set
(r) is ext-real V31() real () set
r + 1 is ext-real V31() real Element of REAL
r + 0 is ext-real V31() real Element of REAL
(r + 1) - 1 is ext-real V31() real Element of REAL
r - 1 is ext-real V31() real Element of REAL
r is ext-real V31() real set
(r) is ext-real V31() real () set
r is ext-real V31() real set
(r) is ext-real V31() real () set
(r) - 1 is ext-real V31() real () Element of REAL
r + 1 is ext-real V31() real Element of REAL
(r) + 0 is ext-real V31() real () Element of REAL
(r + 1) + (- 1) is ext-real V31() real Element of REAL
(r) + (- 1) is ext-real V31() real () Element of REAL
r is ext-real V31() real set
(r) is ext-real V31() real () set
a is ext-real V31() real () set
(r) + a is ext-real V31() real () set
r + a is ext-real V31() real set
((r + a)) is ext-real V31() real () set
r - 1 is ext-real V31() real Element of REAL
(r - 1) + a is ext-real V31() real Element of REAL
(r + a) - 1 is ext-real V31() real Element of REAL
r is ext-real V31() real set
(r) is ext-real V31() real () set
(r) + 1 is ext-real V31() real () Element of REAL
r - 1 is ext-real V31() real Element of REAL
(r - 1) + 1 is ext-real V31() real Element of REAL
r is ext-real V31() real set
r + 1 is ext-real V31() real Element of REAL
r + 0 is ext-real V31() real Element of REAL
(r) is ext-real V31() real () set
(r) + 1 is ext-real V31() real () Element of REAL
a is ext-real V31() real () set
b is ext-real V31() real () set
b is ext-real V31() real set
a is ext-real V31() real () set
b + 1 is ext-real V31() real Element of REAL
a + 1 is ext-real V31() real () Element of REAL
r is ext-real V31() real set
(r) is ext-real V31() real () set
r + 1 is ext-real V31() real Element of REAL
r + 0 is ext-real V31() real Element of REAL
r is ext-real V31() real set
(r) is ext-real V31() real () set
r is ext-real V31() real set
(r) is ext-real V31() real () set
r - 1 is ext-real V31() real Element of REAL
(r) + 1 is ext-real V31() real () Element of REAL
r + 0 is ext-real V31() real Element of REAL
((r) + 1) + (- 1) is ext-real V31() real () Element of REAL
r + (- 1) is ext-real V31() real Element of REAL
r is ext-real V31() real set
(r) is ext-real V31() real () set
a is ext-real V31() real () set
(r) + a is ext-real V31() real () set
r + a is ext-real V31() real set
((r + a)) is ext-real V31() real () set
r + 1 is ext-real V31() real Element of REAL
(r + 1) + a is ext-real V31() real Element of REAL
(r + a) + 1 is ext-real V31() real Element of REAL
r is ext-real V31() real set
(r) is ext-real V31() real () set
(r) is ext-real V31() real () set
r is ext-real V31() real set
(r) is ext-real V31() real () set
(r) is ext-real V31() real () set
r is ext-real V31() real set
(r) is ext-real V31() real () set
(r) is ext-real V31() real () set
r is ext-real V31() real set
(r) is ext-real V31() real () set
((r)) is ext-real V31() real () set
r is ext-real V31() real set
(r) is ext-real V31() real () set
((r)) is ext-real V31() real () set
r is ext-real V31() real set
(r) is ext-real V31() real () set
(r) is ext-real V31() real () set
(r) + 1 is ext-real V31() real () Element of REAL
- (r) is ext-real V31() real () set
(r) + (- (r)) is ext-real V31() real () set
(r) + (- (r)) is ext-real V31() real () set
r - 1 is ext-real V31() real Element of REAL
- (r - 1) is ext-real V31() real Element of REAL
r + 1 is ext-real V31() real Element of REAL
(r + 1) + (- (r - 1)) is ext-real V31() real Element of REAL
((r) + (- (r))) + 1 is ext-real V31() real () Element of REAL
(((r) + (- (r))) + 1) + (- 1) is ext-real V31() real () Element of REAL

(1 + 1) + (- 1) is ext-real V31() real () Element of REAL
(r) + ((r) + (- (r))) is ext-real V31() real () set
r is ext-real V31() real set
(r) is ext-real V31() real () set
r - (r) is ext-real V31() real set
r is ext-real V31() real set
(r) is set
(r) is ext-real V31() real () set
r - (r) is ext-real V31() real set
r is ext-real V31() real set
(r) is ext-real V31() real set
(r) is ext-real V31() real () set
r - (r) is ext-real V31() real set
r is ext-real V31() real set
(r) is ext-real V31() real () set
(r) is ext-real V31() real Element of REAL
r - (r) is ext-real V31() real set
(r) + (r) is ext-real V31() real Element of REAL
r is ext-real V31() real set
(r) is ext-real V31() real Element of REAL
(r) is ext-real V31() real () set
r - (r) is ext-real V31() real set
r - 1 is ext-real V31() real Element of REAL
(r - (r)) + (r) is ext-real V31() real set
(r) + (r - 1) is ext-real V31() real Element of REAL
r - r is ext-real V31() real set
(r) + (- 1) is ext-real V31() real Element of REAL
((r) + (- 1)) + r is ext-real V31() real Element of REAL
(((r) + (- 1)) + r) - r is ext-real V31() real Element of REAL

(r) - 1 is ext-real V31() real Element of REAL
((r) - 1) + 1 is ext-real V31() real Element of REAL
(r) + (r - (r)) is ext-real V31() real set
r + (r) is ext-real V31() real Element of REAL
(r + (r)) - r is ext-real V31() real Element of REAL
r is ext-real V31() real set
(r) is ext-real V31() real Element of REAL
(r) is ext-real V31() real () set
r - (r) is ext-real V31() real set
((r)) is ext-real V31() real () set
- (r) is ext-real V31() real () set
r + (- (r)) is ext-real V31() real set
((r + (- (r)))) is ext-real V31() real () set
(r) + (- (r)) is ext-real V31() real () set
r is ext-real V31() real set
(r) is ext-real V31() real Element of REAL
(r) is ext-real V31() real () set
r - (r) is ext-real V31() real set
r is ext-real V31() real set
(r) is ext-real V31() real Element of REAL
(r) is ext-real V31() real () set
r - (r) is ext-real V31() real set
r is ext-real V31() real () set
a is ext-real V31() real () set
r / a is ext-real V31() real set
((r / a)) is ext-real V31() real () set
a is ext-real V31() real () set
r is ext-real V31() real () set
(r,a) is ext-real V31() real () set
r / a is ext-real V31() real set
((r / a)) is ext-real V31() real () set
(r,a) * a is ext-real V31() real () set
r - ((r,a) * a) is ext-real V31() real () set
r is ext-real V31() real set
r / r is ext-real V31() real set
((r / r)) is ext-real V31() real () set
(1) is ext-real V31() real () set
r is ext-real V31() real () set
(r,0) is ext-real V31() real () set
r / 0 is ext-real V31() real set
((r / 0)) is ext-real V31() real () set
r / 0 is ext-real V31() real Element of REAL
0 " is ext-real non negative V31() real Element of REAL
r * () is ext-real V31() real Element of REAL
r * 0 is ext-real V31() real () Element of REAL
0 - 1 is ext-real V31() real () Element of REAL
r is ext-real V31() real () set
(r,r) is ext-real V31() real () set
r / r is ext-real V31() real set
((r / r)) is ext-real V31() real () set
r is ext-real V31() real () set
(r,r) is ext-real V31() real () set
(r,r) is ext-real V31() real () set
r / r is ext-real V31() real set
((r / r)) is ext-real V31() real () set
(r,r) * r is ext-real V31() real () set
r - ((r,r) * r) is ext-real V31() real () set
1 * r is ext-real V31() real () Element of REAL
r - (1 * r) is ext-real V31() real () Element of REAL
a is ext-real V31() real () set
r is ext-real V31() real () set
a - r is ext-real V31() real () set
r - r is ext-real V31() real () set

09 is ext-real V31() real () set
09 + 1 is ext-real V31() real () Element of REAL
j9 is ext-real V31() real () set
a is ext-real V31() real () set
r is ext-real V31() real () set
a - 1 is ext-real V31() real () Element of REAL
r - 1 is ext-real V31() real () Element of REAL
(r - 1) + 1 is ext-real V31() real () Element of REAL
r is ext-real V31() real set
(r) is ext-real V31() real () set
(r) is ext-real V31() real () set
r - 1 is ext-real V31() real Element of REAL
(r) + 1 is ext-real V31() real () Element of REAL
(r - 1) + 1 is ext-real V31() real Element of REAL
((r) + 1) - 1 is ext-real V31() real () Element of REAL
0 - 1 is ext-real V31() real () Element of REAL
r is ext-real V31() real () set
a is ext-real V31() real set
(a) is ext-real V31() real () set
r - 1 is ext-real V31() real () Element of REAL
a - 1 is ext-real V31() real Element of REAL
(r - 1) + 1 is ext-real V31() real () Element of REAL

(r,a) is ext-real V31() real () set
r / a is ext-real non negative V31() real set
((r / a)) is ext-real V31() real () set
r is ext-real V31() real () set
a is ext-real V31() real () set
(r,a) is ext-real V31() real () set
r / a is ext-real V31() real set
((r / a)) is ext-real V31() real () set
a * (r,a) is ext-real V31() real () set
a * (r / a) is ext-real V31() real set
(r,a) " is ext-real V31() real set
(a * (r,a)) * ((r,a) ") is ext-real V31() real set
(r,a) * ((r,a) ") is ext-real V31() real set
a * ((r,a) * ((r,a) ")) is ext-real V31() real set
a * 1 is ext-real V31() real () Element of REAL
r is ext-real V31() real () set
a is ext-real V31() real () set
(a,r) is ext-real V31() real () set
a / r is ext-real V31() real set
((a / r)) is ext-real V31() real () set
(a,r) is ext-real V31() real () set
(a,r) * r is ext-real V31() real () set
(a / r) * r is ext-real V31() real set
a - ((a,r) * r) is ext-real V31() real () set
r is ext-real V31() real () set
a is ext-real V31() real () set
(a,r) is ext-real V31() real () set
a / r is ext-real V31() real set
((a / r)) is ext-real V31() real () set
(a / r) - 1 is ext-real V31() real Element of REAL
(a,r) is ext-real V31() real () set
(a,r) * r is ext-real V31() real () set
((a / r) - 1) * r is ext-real V31() real Element of REAL
(a / r) * r is ext-real V31() real set
1 * r is ext-real V31() real () Element of REAL
((a / r) * r) - (1 * r) is ext-real V31() real Element of REAL
((a,r) * r) - 0 is ext-real V31() real () Element of REAL
a - r is ext-real V31() real () set
r - 0 is ext-real V31() real () Element of REAL
a - ((a,r) * r) is ext-real V31() real () set
r is ext-real V31() real () set
a is ext-real V31() real () set
(a,r) is ext-real V31() real () set
a / r is ext-real V31() real set
((a / r)) is ext-real V31() real () set
(a,r) * r is ext-real V31() real () set
(a,r) is ext-real V31() real () set
((a,r) * r) + (a,r) is ext-real V31() real () set
a - ((a,r) * r) is ext-real V31() real () set
((a,r) * r) + (a - ((a,r) * r)) is ext-real V31() real () set
r is ext-real V31() real () set
a is ext-real V31() real () set
r * a is ext-real V31() real () set
(r * a) - 0 is ext-real V31() real () set
(r * a) - 0 is ext-real V31() real () Element of REAL
r is ext-real V31() real () set
a is ext-real V31() real () set
(r,a) is ext-real V31() real () set
r / a is ext-real V31() real set
((r / a)) is ext-real V31() real () set
(r / a) - 1 is ext-real V31() real Element of REAL
0 - 1 is ext-real V31() real () Element of REAL

a is ext-real V31() real () set
(a,r) is ext-real V31() real () set
(a,r) is ext-real V31() real () set
a / r is ext-real V31() real set
((a / r)) is ext-real V31() real () set
(a,r) * r is ext-real V31() real () set
a - ((a,r) * r) is ext-real V31() real () set
((a / r)) * r is ext-real V31() real () set
a - (((a / r)) * r) is ext-real V31() real () set
b is ext-real V31() real () set
r * b is ext-real V31() real () set
- r is ext-real non positive V31() real () set
0 + a is ext-real V31() real () Element of REAL
(- r) + a is ext-real V31() real () set
r " is ext-real non negative V31() real set
(r * b) * (r ") is ext-real V31() real set
((- r) + a) * (r ") is ext-real V31() real set
(- r) * (r ") is ext-real non positive V31() real set
a * (r ") is ext-real V31() real set
((- r) * (r ")) + (a * (r ")) is ext-real V31() real set
r * (r ") is ext-real non negative V31() real set
(r * (r ")) * b is ext-real V31() real set
((- r) * (r ")) + (a / r) is ext-real V31() real set
1 * b is ext-real V31() real () Element of REAL
- (r * (r ")) is ext-real non positive V31() real set
(- (r * (r "))) + (a / r) is ext-real V31() real set
(- 1) + (a / r) is ext-real V31() real Element of REAL
(a / r) - 1 is ext-real V31() real Element of REAL
b * r is ext-real V31() real () set
(a / r) * r is ext-real V31() real set
(a * (r ")) * r is ext-real V31() real set
(r ") * r is ext-real non negative V31() real set
a * ((r ") * r) is ext-real V31() real set
a * 1 is ext-real V31() real () Element of REAL
r is ext-real V31() real set
- r is ext-real V31() real set
a is ext-real V31() real set
r / a is ext-real V31() real set
((r / a)) is ext-real V31() real () set
- ((r / a)) is ext-real V31() real () set
(- r) / a is ext-real V31() real set
(((- r) / a)) is ext-real V31() real () set
(((- r) / a)) + 1 is ext-real V31() real () Element of REAL
(r / a) - 1 is ext-real V31() real Element of REAL
- ((r / a) - 1) is ext-real V31() real Element of REAL
- (r / a) is ext-real V31() real set
(- (r / a)) + 1 is ext-real V31() real Element of REAL
((- r) / a) + 1 is ext-real V31() real Element of REAL
(- ((r / a))) - 1 is ext-real V31() real () Element of REAL
(((- r) / a) + 1) - 1 is ext-real V31() real Element of REAL
(- (r / a)) - 1 is ext-real V31() real Element of REAL
((- r) / a) - 1 is ext-real V31() real Element of REAL
((- ((r / a))) - 1) + 1 is ext-real V31() real () Element of REAL
r is ext-real V31() real set
- r is ext-real V31() real set
a is ext-real V31() real set
r / a is ext-real V31() real set
((r / a)) is ext-real V31() real () set
- ((r / a)) is ext-real V31() real () set
(- r) / a is ext-real V31() real set
(((- r) / a)) is ext-real V31() real () set
- (r / a) is ext-real V31() real set
(- ((r / a))) - 0 is ext-real V31() real () Element of REAL
((- r) / a) - 1 is ext-real V31() real Element of REAL
r is ext-real V31() real () set
a is ext-real V31() real set
(a) is ext-real V31() real () set
a + 1 is ext-real V31() real Element of REAL
r + 1 is ext-real V31() real () Element of REAL
(r + 1) - 1 is ext-real V31() real () Element of REAL

(F1() + 1) - 1 is ext-real V31() real () Element of REAL
r - 1 is ext-real V31() real () Element of REAL

(r - 1) + 1 is ext-real V31() real () Element of REAL

r is ext-real V31() real () set
a is ext-real V31() real set
a + r is ext-real V31() real set
((a + r)) is ext-real V31() real Element of REAL
((a + r)) is ext-real V31() real () set
(a + r) - ((a + r)) is ext-real V31() real set
(a) is ext-real V31() real Element of REAL
(a) is ext-real V31() real () set
a - (a) is ext-real V31() real set
(a) + r is ext-real V31() real () set
(a + r) - ((a) + r) is ext-real V31() real set
(a - (a)) + r is ext-real V31() real set
((a - (a)) + r) - r is ext-real V31() real set
r is ext-real V31() real set
(r) is ext-real V31() real () set
(r) + 1 is ext-real V31() real () Element of REAL
a is ext-real V31() real set
(a) is ext-real V31() real () set
((r) + 1) - 1 is ext-real V31() real () Element of REAL
a - 1 is ext-real V31() real Element of REAL
r is ext-real V31() real set
(r) is ext-real V31() real () set
(r) + 1 is ext-real V31() real () Element of REAL
(r) is ext-real V31() real Element of REAL
r - (r) is ext-real V31() real set
a is ext-real V31() real set
(a) is ext-real V31() real Element of REAL
(a) is ext-real V31() real () set
a - (a) is ext-real V31() real set
r is ext-real V31() real set
(r) is ext-real V31() real () set
(r) + 1 is ext-real V31() real () Element of REAL
(r) is ext-real V31() real Element of REAL
r - (r) is ext-real V31() real set
a is ext-real V31() real set
(a) is ext-real V31() real Element of REAL
(a) is ext-real V31() real () set
a - (a) is ext-real V31() real set
r is ext-real V31() real set
(r) is ext-real V31() real () set
a is ext-real V31() real set
(a) is ext-real V31() real () set
(a) + 1 is ext-real V31() real () Element of REAL
a + 1 is ext-real V31() real Element of REAL
r - 1 is ext-real V31() real Element of REAL
(a + 1) - 1 is ext-real V31() real Element of REAL
r is ext-real V31() real set
(r) is ext-real V31() real Element of REAL
(r) is ext-real V31() real () set
r - (r) is ext-real V31() real set
a is ext-real V31() real set
(a) is ext-real V31() real () set
(a) + 1 is ext-real V31() real () Element of REAL
a + 1 is ext-real V31() real Element of REAL
(a) is ext-real V31() real Element of REAL
a - (a) is ext-real V31() real set
r - 1 is ext-real V31() real Element of REAL
(r - 1) - (a) is ext-real V31() real Element of REAL
r is ext-real V31() real set
r + 1 is ext-real V31() real Element of REAL
a is ext-real V31() real set
(a) is ext-real V31() real Element of REAL
(a) is ext-real V31() real () set
a - (a) is ext-real V31() real set
b is ext-real V31() real set
(b) is ext-real V31() real Element of REAL
(b) is ext-real V31() real () set
b - (b) is ext-real V31() real set
(r) is ext-real V31() real () set
(r) + 1 is ext-real V31() real () Element of REAL
(r) is ext-real V31() real Element of REAL
r - (r) is ext-real V31() real set
(r) + 1 is ext-real V31() real () Element of REAL
(r) is ext-real V31() real Element of REAL
r - (r) is ext-real V31() real set
(r) + 1 is ext-real V31() real () Element of REAL
((r) + 1) - 1 is ext-real V31() real () Element of REAL
b - 1 is ext-real V31() real Element of REAL
a - 1 is ext-real V31() real Element of REAL
(r) + 1 is ext-real V31() real () Element of REAL
(r) + 1 is ext-real V31() real () Element of REAL