:: XREAL_1 semantic presentation

REAL is non empty set

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

{K105()} is non empty set
is set

is non empty set

-infty is non empty ext-real non positive negative non real set
is set
+infty is non empty ext-real positive non negative non real set

b is Element of REAL+
c is Element of REAL+
q is Element of REAL+
[0,q] is set
p is Element of REAL+
[0,p] is set
b is Element of REAL+
c is Element of REAL+
q is Element of REAL+
[0,q] is set
p is Element of REAL+
[0,p] is set
b is Element of REAL+
c is Element of REAL+
q is Element of REAL+
[0,q] is set
p is Element of REAL+
[0,p] is set

[*a,b*] is complex Element of COMPLEX
(0,1) --> (a,b) is V6() V18({0,1}, REAL ) Element of bool [:{0,1},REAL:]
{0,1} is non empty set
[:{0,1},REAL:] is set
bool [:{0,1},REAL:] is set

+ (o,a) is complex ext-real real Element of REAL

[*q,p*] is complex Element of COMPLEX

[*c7,b9*] is complex Element of COMPLEX
+ (q,c7) is complex ext-real real Element of REAL
+ (p,b9) is complex ext-real real Element of REAL
[*(+ (q,c7)),(+ (p,b9))*] is complex Element of COMPLEX

is non empty set

+ (q,p) is complex ext-real real Element of REAL

+ (c,p) is complex ext-real real Element of REAL
c7 is Element of REAL+
b9 is Element of REAL+
c7 + b9 is Element of REAL+
c99 is Element of REAL+
a99 is Element of REAL+
c99 + a99 is Element of REAL+
b99 is Element of REAL+
a9 is Element of REAL+
c7 is Element of REAL+
b9 is Element of REAL+
c7 + b9 is Element of REAL+
c99 is Element of REAL+
[0,c99] is set
a99 is Element of REAL+
a99 - c99 is set
a99 -' c99 is Element of REAL+
c99 -' a99 is Element of REAL+
[0,(c99 -' a99)] is set
c7 is Element of REAL+
[0,c7] is set
b9 is Element of REAL+
b9 - c7 is set
c99 is Element of REAL+
[0,c99] is set
a99 is Element of REAL+
[0,a99] is set
b99 is Element of REAL+
[0,b99] is set
a9 is Element of REAL+
a9 - b99 is set
a9 - c7 is set
a9 -' c7 is Element of REAL+
a9 -' b99 is Element of REAL+
b9 -' c7 is Element of REAL+
b99 -' a9 is Element of REAL+
[0,(b99 -' a9)] is set
a9 - c7 is set
a9 -' c7 is Element of REAL+
c7 -' a9 is Element of REAL+
[0,(c7 -' a9)] is set
c7 is Element of REAL+
b9 is Element of REAL+
[0,b9] is set
c7 - b9 is set
c99 is Element of REAL+
a99 is Element of REAL+
[0,a99] is set
c99 - a99 is set
b99 is Element of REAL+
a9 is Element of REAL+
c7 - a99 is set
c7 -' a99 is Element of REAL+
c99 -' a99 is Element of REAL+
c7 -' b9 is Element of REAL+
b99 is Element of REAL+
a9 is Element of REAL+
a99 -' c99 is Element of REAL+
[0,(a99 -' c99)] is set
c7 - a99 is set
c7 -' a99 is Element of REAL+
a99 -' c7 is Element of REAL+
b99 is Element of REAL+
a9 is Element of REAL+
[0,(a99 -' c7)] is set
c7 is Element of REAL+
[0,c7] is set
b9 is Element of REAL+
[0,b9] is set
c7 + b9 is Element of REAL+
[0,(c7 + b9)] is set
c99 is Element of REAL+
a99 is Element of REAL+
[0,a99] is set
c99 - a99 is set
c99 -' a99 is Element of REAL+
b9 + c7 is Element of REAL+
b9 -' c99 is Element of REAL+
[0,(b9 -' c99)] is set
c7 is Element of REAL+
[0,c7] is set
b9 is Element of REAL+
[0,b9] is set
c7 + b9 is Element of REAL+
[0,(c7 + b9)] is set
c99 is Element of REAL+
[0,c99] is set
a99 is Element of REAL+
[0,a99] is set
c99 + a99 is Element of REAL+
[0,(c99 + a99)] is set
b99 is Element of REAL+
[0,b99] is set
a9 is Element of REAL+
[0,a9] is set
c99 + b9 is Element of REAL+
c7 + a99 is Element of REAL+

o + (- b) is complex ext-real real set
a + (- b) is complex ext-real real set

(q + c7) - b9 is complex ext-real real set

(q + b9) - b9 is complex ext-real real set

- 1 is non empty complex ext-real non positive negative real set
o + (- 1) is complex ext-real real set

(o + a) + (- a) is complex ext-real real set
(b + a) + (- a) is complex ext-real real set

- 1 is non empty complex ext-real non positive negative real set
o + (- 1) is complex ext-real real set

- 1 is non empty complex ext-real non positive negative real set
a + (- 1) is complex ext-real real set

* (o,a) is complex ext-real real Element of REAL

[*q,p*] is complex Element of COMPLEX

[*c7,b9*] is complex Element of COMPLEX
* (q,c7) is complex ext-real real Element of REAL
* (p,b9) is complex ext-real real Element of REAL
opp (* (p,b9)) is complex ext-real real Element of REAL
+ ((* (q,c7)),(opp (* (p,b9)))) is complex ext-real real Element of REAL
* (q,b9) is complex ext-real real Element of REAL
* (p,c7) is complex ext-real real Element of REAL
+ ((* (q,b9)),(* (p,c7))) is complex ext-real real Element of REAL
[*(+ ((* (q,c7)),(opp (* (p,b9))))),(+ ((* (q,b9)),(* (p,c7))))*] is complex Element of COMPLEX

* ((opp p),b9) is complex ext-real real Element of REAL
+ ((* (q,c7)),(* ((opp p),b9))) is complex ext-real real Element of REAL

o is Element of REAL+

* (p,c7) is complex ext-real real Element of REAL

* (q,c7) is complex ext-real real Element of REAL
b9 is Element of REAL+
c99 is Element of REAL+
b9 *' c99 is Element of REAL+
a99 is Element of REAL+
b99 is Element of REAL+
a99 *' b99 is Element of REAL+
b9 *' b99 is Element of REAL+
a9 is Element of REAL+
c9 is Element of REAL+
b9 is Element of REAL+
[0,b9] is set
c99 is Element of REAL+
c99 *' b9 is Element of REAL+
[0,(c99 *' b9)] is set
b9 is Element of REAL+
c99 is Element of REAL+
b9 *' c99 is Element of REAL+
b9 is Element of REAL+
[0,b9] is set
c99 is Element of REAL+
c99 *' b9 is Element of REAL+
[0,(c99 *' b9)] is set
a99 is Element of REAL+
[0,a99] is set
b99 is Element of REAL+
[0,b99] is set
a9 is Element of REAL+
[0,a9] is set
c9 is Element of REAL+
c9 *' a9 is Element of REAL+
[0,(c9 *' a9)] is set
b9 *' c9 is Element of REAL+
a9 *' c9 is Element of REAL+

a * (a ") is complex ext-real real set
b * (a * (a ")) is complex ext-real real set
(c * a) * (a ") is complex ext-real real set

c * (a * (a ")) is complex ext-real real set

(a + b) / 2 is complex ext-real real set

(1 * a) + a is complex ext-real real set
2 " is non empty complex ext-real positive non negative real set
(2 ") * (a + b) is complex ext-real real set

(2 ") * (2 * a) is complex ext-real real set

(1 * b) + b is complex ext-real real set

(2 ") * (2 * b) is complex ext-real real set

(a - b) - a is complex ext-real real set

- (- b) is complex ext-real real set
- (- a) is complex ext-real real set

a + (- c) is complex ext-real real set
(a + (- c)) + c is complex ext-real real set
b + (- c) is complex ext-real real set
(b + (- c)) + c is complex ext-real real set

- (c - a) is complex ext-real real set
- (c - b) is complex ext-real real set

(a + b) - b is complex ext-real real set

(b - c) + c is complex ext-real real set

(c + b) - b is complex ext-real real set

a + (- b) is complex ext-real real set
c - (- b) is complex ext-real real set

a + (- q) is complex ext-real real set
b + (- c) is complex ext-real real set

b + (- c) is complex ext-real real set
a + (- q) is complex ext-real real set

- (c - b) is complex ext-real real set
- (q - a) is complex ext-real real set

(c + q) - b is complex ext-real real set
c + (q - b) is complex ext-real real set

(a - b) + q is complex ext-real real set

(a + q) - b is complex ext-real real set

(a - b) + q is complex ext-real real set

(a + q) - b is complex ext-real real set

(a - b) + q is complex ext-real real set

(a + q) - b is complex ext-real real set

(b + a) - c is complex ext-real real set
b + (a - c) is complex ext-real real set

(a + b) + q is complex ext-real real set
(a + q) + b is complex ext-real real set

(a + b) + q is complex ext-real real set
(a + q) + b is complex ext-real real set

(c + q) + b is complex ext-real real set
(c + b) + q is complex ext-real real set

(c + q) + b is complex ext-real real set
(c + b) + q is complex ext-real real set

(- b) + b is complex ext-real real set
b - (- a) is complex ext-real real set

(- b) + b is complex ext-real real set

b - (- a) is complex ext-real real set

(a - b) + b is complex ext-real real set

(a + b) - b is complex ext-real real set

b + (- a) is complex ext-real real set
(b + (- a)) - b is complex ext-real real set

c * (- a) is complex ext-real real set
b * (- a) is complex ext-real real set
- (c * a) is complex ext-real real set
- (b * a) is complex ext-real real set

b * (a ") is complex ext-real real set
c * (a ") is complex ext-real real set
(b / a) * a is complex ext-real real set
(c / a) * a is complex ext-real real set

c * (a ") is complex ext-real real set
b * (a ") is complex ext-real real set

(a / 2) + (a / 2) is complex ext-real real set
0 + (a / 2) is complex ext-real real set

b + (a - b) is complex ext-real real set
(a - b) / 2 is complex ext-real real set
b + ((a - b) / 2) is complex ext-real real set

- (b - a) is complex ext-real real set
(- (b - a)) / 2 is complex ext-real real set
b + (- (b - a)) is complex ext-real real set
(b - a) / 2 is complex ext-real real set
- ((b - a) / 2) is complex ext-real real set
b + (- ((b - a) / 2)) is complex ext-real real set
b - (b - a) is complex ext-real real set
b - ((b - a) / 2) is complex ext-real real set
a + ((b - a) / 2) is complex ext-real real set

b + (- a) is complex ext-real real set

(a - b) + b is complex ext-real real set

- (b - a) is complex ext-real real set
(- (b - a)) / 2 is complex ext-real real set
b + (- (b - a)) is complex ext-real real set
(b - a) / 2 is complex ext-real real set
- ((b - a) / 2) is complex ext-real real set
b + (- ((b - a) / 2)) is complex ext-real real set
b - (b - a) is complex ext-real real set
b - ((b - a) / 2) is complex ext-real real set

b + (a - b) is complex ext-real real set
(a - b) / 2 is complex ext-real real set
b + ((a - b) / 2) is complex ext-real real set
a - ((a - b) / 2) is complex ext-real real set

(- b) + b is complex ext-real real set

(- a) + a is complex ext-real real set

(- b) + b is complex ext-real real set

(- a) + a is complex ext-real real set

a * (- c) is complex ext-real real set
b * (- c) is complex ext-real real set
- (a * c) is complex ext-real real set
- (b * c) is complex ext-real real set

(- a) * (- c) is complex ext-real real set
(- b) * (- q) is complex ext-real real set

(a * c) + (b * q) is complex ext-real real set

c / (- a) is complex ext-real real set
b / (- a) is complex ext-real real set
- (b / a) is complex ext-real real set
- (c / a) is complex ext-real real set

c * (a ") is complex ext-real real set
b * (a ") is complex ext-real real set
(b / a) * a is complex ext-real real set
(c / a) * a is complex ext-real real set

c * (c ") is complex ext-real real set
b * (c ") is complex ext-real real set

(b ") * 1 is complex ext-real real set
(b ") * (b * (c ")) is complex ext-real real set
(b ") * b is complex ext-real real set
((b ") * b) * (c ") is complex ext-real real set
1 * (c ") is complex ext-real real set
a * (b ") is complex ext-real real set
a * (c ") is complex ext-real real set

b * (b ") is complex ext-real real set
a * (b ") is complex ext-real real set
(a ") * (a * (b ")) is complex ext-real real set
1 * (a ") is complex ext-real real set
(a ") * a is complex ext-real real set
((a ") * a) * (b ") is complex ext-real real set
1 * (b ") is complex ext-real real set

(b * a) / a is complex ext-real real set

(b * a) / a is complex ext-real real set

(c * a) / a is complex ext-real real set

(c * a) / a is complex ext-real real set

(b * a) / a is complex ext-real real set

(b * a) / a is complex ext-real real set

(c * a) / a is complex ext-real real set

(c * a) / a is complex ext-real real set

a * (b ") is complex ext-real real set
b * (b ") is complex ext-real real set
(a ") * (a * (b ")) is complex ext-real real set
1 * (a ") is complex ext-real real set
(a ") * a is complex ext-real real set
((a ") * a) * (b ") is complex ext-real real set
1 * (b ") is complex ext-real real set

a * (b ") is complex ext-real real set
b * (b ") is complex ext-real real set
1 * (a ") is complex ext-real real set
(a ") * (a * (b ")) is complex ext-real real set
(a ") * a is complex ext-real real set
((a ") * a) * (b ") is complex ext-real real set
1 * (b ") is complex ext-real real set

b * (b ") is complex ext-real real set
a * (b ") is complex ext-real real set
1 * (a ") is complex ext-real real set
(a ") * (a * (b ")) is complex ext-real real set
(a ") * a is complex ext-real real set
((a ") * a) * (b ") is complex ext-real real set
1 * (b ") is complex ext-real real set

(b ") " is complex ext-real real set
(a ") " is complex ext-real real set

(a ") " is complex ext-real real set
(b ") " is complex ext-real real set

(a ") " is complex ext-real real set
(b ") " is complex ext-real real set

(b ") " is complex ext-real real set
(a ") " is complex ext-real real set

(b - a) * (b + a) is complex ext-real real set

(b - a) * (b + a) is complex ext-real real set

(a - b) * (a + b) is complex ext-real real set

(a - b) + b is complex ext-real real set
(a + b) - b is complex ext-real real set

(c ") * a is complex ext-real real set
(b ") * a is complex ext-real real set

(c ") * a is complex ext-real real set
(b ") * a is complex ext-real real set

(b ") * a is complex ext-real real set
(c ") * a is complex ext-real real set

(c * b) / a is complex ext-real real set
(c / a) * b is complex ext-real real set

(c * b) / a is complex ext-real real set
(c / a) * b is complex ext-real real set

(c * b) / a is complex ext-real real set
(c / a) * b is complex ext-real real set

(c * b) / a is complex ext-real real set
(c / a) * b is complex ext-real real set

(c * b) / a is complex ext-real real set
(c / a) * b is complex ext-real real set

(c * b) / a is complex ext-real real set
(c / a) * b is complex ext-real real set

(c * b) / a is complex ext-real real set
(c / a) * b is complex ext-real real set

(c * b) / a is complex ext-real real set
(c / a) * b is complex ext-real real set

(c * a) * b is complex ext-real real set
(c * b) * a is complex ext-real real set

(c * a) * b is complex ext-real real set
(c * b) * a is complex ext-real real set

(q * a) * b is complex ext-real real set
(q * b) * a is complex ext-real real set

(q * a) * b is complex ext-real real set
(q * b) * a is complex ext-real real set

(c * a) * b is complex ext-real real set
(c * b) * a is complex ext-real real set

(c * a) * b is complex ext-real real set
(c * b) * a is complex ext-real real set

(q * a) * b is complex ext-real real set
(q * b) * a is complex ext-real real set

(q * a) * b is complex ext-real real set
(q * b) * a is complex ext-real real set

a * (c ") is complex ext-real real set
c * (c ") is complex ext-real real set

(a ") * (a * (c ")) is complex ext-real real set
(a ") * 1 is complex ext-real real set
(a ") * a is complex ext-real real set
((a ") * a) * (c ") is complex ext-real real set
1 * (c ") is complex ext-real real set
b * (c ") is complex ext-real real set
b * (a ") is complex ext-real real set

(b ") * a is complex ext-real real set
(c ") * a is complex ext-real real set

(b ") * a is complex ext-real real set
(c ") * a is complex ext-real real set

(c ") * a is complex ext-real real set
(b ") * a is complex ext-real real set

(b ") " is complex ext-real real set
(a ") " is complex ext-real real set

a * (b ") is complex ext-real real set

a * (b ") is complex ext-real real set

(b - 1) + 1 is complex ext-real real set
(a - 1) + 1 is complex ext-real real set

- 1 is non empty complex ext-real non positive negative real set
a + (- 1) is complex ext-real real set

(b - 1) + 1 is complex ext-real real set
- 1 is non empty complex ext-real non positive negative real set

(- 1) + 1 is complex ext-real real set

1 " is non empty complex ext-real positive non negative real set