:: 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₆ is Element of REAL+
[0,c₆] is set
{0,c₆} is set
{{0,c₆},{0}} is set
i9 is Element of REAL+
i9 - c₆ 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 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₆ is ext-real V31() real Element of REAL
i9 is ext-real V31() real Element of REAL
[*c₆,i9*] is Element of COMPLEX
+ (j9,c₆) is ext-real V31() real Element of REAL
+ (09,i9) is ext-real V31() real Element of REAL
[*(+ (j9,c₆)),(+ (09,i9))*] is Element of COMPLEX
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₁() is ext-real V31() real () set
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₁() is ext-real V31() real () set
b - 1 is ext-real V31() real () Element of REAL
a is ext-real V31() real () set
a + F₁() is ext-real V31() real () set
(b - 1) - F₁() 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 - F₁() 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 ext-real V31() real () set
b - F₁() is ext-real V31() real () set
F₁() is ext-real V31() real () set
- F₁() 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
- (- F₁()) 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
F₁() 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
F₁() is ext-real V31() real () set
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 ext-real V31() real () Element of REAL
a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () set
F₁() + a is ext-real V31() real () set
b is ext-real V31() real () set
j9 is ext-real V31() real () set
b - F₁() is ext-real V31() real () set
j9 - F₁() is ext-real V31() real () set
09 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT
F₁() + 09 is ext-real V31() real () Element of REAL
j9 is ext-real V31() real () set
F₁() is ext-real V31() real () set
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 ext-real V31() real () Element of REAL
a is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () set
F₁() - a is ext-real V31() real () set
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₁() - 09 is ext-real V31() real () Element of REAL
- b is ext-real V31() real () set
F₁() + (- b) is ext-real V31() real () set
(F₁() + (- b)) - F₁() is ext-real V31() real () set
F₁() - j9 is ext-real V31() real () set
(F₁() - j9) - F₁() is ext-real V31() real () set
- j9 is ext-real V31() real () set
F₁() + (- j9) is ext-real V31() real () set
(F₁() + (- j9)) - F₁() 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
c₆ is ext-real V31() real () set
b * c₆ is ext-real V31() real () set
09 + c₆ is ext-real V31() real () set
b * (09 + c₆) 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
c₆ is ext-real V31() real () set
b * c₆ 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
c₆ + i9 is ext-real V31() real () set
b * (c₆ + 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
c₆ is ext-real V31() real () set
b * c₆ 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
c₆ - i9 is ext-real V31() real () set
b * (c₆ - 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
c₆ is ext-real V31() real () set
b * c₆ 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 * c₆) * j9 is ext-real V31() real () set
(b * i9) * a is ext-real V31() real () set
((b * c₆) * j9) + ((b * i9) * a) is ext-real V31() real () set
c₆ * j9 is ext-real V31() real () set
i9 * a is ext-real V31() real () set
(c₆ * j9) + (i9 * a) is ext-real V31() real () set
b * ((c₆ * 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
c₆ is ext-real V31() real () set
b * c₆ is ext-real V31() real () set
a * c₆ is ext-real V31() real () set
r * (a * c₆) 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
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₁() is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT
F₂() 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 () set
F₁() + 1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V31() real () Element of NAT
(F₁() + 1) - 1 is ext-real V31() real () Element of REAL
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₁() is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V31() real () Element of NAT
F₂() 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 + 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