:: INT_1 semantic presentation

REAL is non empty V33() set

NAT is non empty epsilon-transitive epsilon-connected ordinal Element of bool REAL

bool REAL is set

omega is non empty epsilon-transitive epsilon-connected ordinal 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

bool omega is set

1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V31() real Element of NAT

0 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real Element of NAT

the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V31() real set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V31() real set

{} is set

{{}} is set

[:{{}},REAL+:] is set

REAL+ \/ [:{{}},REAL+:] is set

[{},{}] is set

{{},{}} is set

{{{},{}},{{}}} is set

{[{},{}]} is set

(REAL+ \/ [:{{}},REAL+:]) \ {[{},{}]} is Element of bool (REAL+ \/ [:{{}},REAL+:])

bool (REAL+ \/ [:{{}},REAL+:]) is set

INT is non empty V33() set

[:{{}},omega:] is set

omega \/ [:{{}},omega:] is set

(omega \/ [:{{}},omega:]) \ {[{},{}]} is Element of bool (omega \/ [:{{}},omega:])

bool (omega \/ [:{{}},omega:]) is set

K105() is Element of K99()

{0} is set

[:{0},REAL+:] is set

[:{0},NAT:] is set

[0,0] is set

{0,0} is set

{{0,0},{0}} is set

{[0,0]} is set

[:{0},NAT:] \ {[0,0]} is Element of bool [:{0},NAT:]

bool [:{0},NAT:] is set

r is set

NAT \/ [:{0},NAT:] 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

09 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real Element of NAT

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

c

[0,c

{0,c

{{0,c

i9 is Element of REAL+

i9 - c

- 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 epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real Element of NAT

- 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

c

i9 is ext-real V31() real Element of REAL

[*c

+ (j9,c

+ (09,i9) is ext-real V31() real Element of REAL

[*(+ (j9,c

x9 is Element of REAL+

y9 is Element of REAL+

x9 + y9 is Element of REAL+

REAL+ \/ [:{0},REAL+:] is set

x9 is Element of REAL+

[0,x9] is set

{0,x9} is set

{{0,x9},{0}} is set

y9 is Element of REAL+

y9 - x9 is set

r is set

a is set

b is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real Element of NAT

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

NAT \/ [:{0},NAT:] is set

NAT \/ [:{0},NAT:] is set

a is set

b is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real Element of NAT

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

NAT \/ [:{0},NAT:] is set

NAT \/ [:{0},NAT:] is set

a is set

b is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real Element of NAT

j9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real Element of NAT

- 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 epsilon-transitive epsilon-connected ordinal natural ext-real non negative 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 epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

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

j9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

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

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

0 + j9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

09 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () set

b + 09 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

- 09 is ext-real non positive V31() real set

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

09 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () set

j9 + 09 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

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

0 + b is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

09 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () set

j9 + 09 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

- 09 is ext-real non positive V31() real set

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

09 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () set

b + 09 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

j9 + b is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

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

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

b is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

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

j9 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

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

j9 * b is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

- (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

a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

b is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

- 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 epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

- 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

r is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

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 epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V31() real () Element of NAT

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

a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

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

b is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

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

b is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

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

bool INT is set

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

F

r is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

r + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V31() real () Element of NAT

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

b - F

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

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

a + F

(b - 1) - F

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

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

r - F

a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

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

b - F

F

- F

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

- (- F

(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

F

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

F

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

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

a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

F

a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () set

F

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

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

b - F

j9 - F

09 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

F

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

F

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

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

a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

F

a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () set

F

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

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

09 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

F

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

F

(F

F

(F

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

F

(F

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

c

b * c

09 + c

b * (09 + c

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

c

b * c

j9 - 09 is ext-real V31() real () set

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

b * i9 is ext-real V31() real () set

c

b * (c

(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

c

b * c

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

c

b * (c

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

c

b * c

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 * c

(b * i9) * a is ext-real V31() real () set

((b * c

c

i9 * a is ext-real V31() real () set

(c

b * ((c

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

c

b * c

a * c

r * (a * c

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

09 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

r is ext-real V31() real set

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

- r is ext-real V31() real set

a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

- (- 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 epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

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 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V31() real () Element of NAT

(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

0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V31() real () Element of NAT

(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 * (0 ") 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

b is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

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 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () set

a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () set

(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

r is epsilon-transitive epsilon-connected ordinal natural ext-real non negative 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 - ((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

F

F

r is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

r is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () set

F

(F

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

a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

a + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V31() real () Element of NAT

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

r + 0 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

F

F

r is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

r + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V31() real () Element of NAT

a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

r is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

r is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT

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