:: XREAL_1 semantic presentation

REAL is non empty 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 non empty Element of bool (bool K99())

REAL+ is non empty set

COMPLEX is non empty set

K105() is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real Element of K99()

K106() is non empty epsilon-transitive epsilon-connected ordinal Element of K99()

{K105()} is non empty set

[:{K105()},REAL+:] is set

0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real Element of NAT

{0} is non empty set

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

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

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

[0,REAL] is set

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

o is complex ext-real real set

a is complex ext-real 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

o is complex ext-real real set

a is complex ext-real real Element of REAL

b is complex ext-real real Element of REAL

[*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 is complex ext-real real Element of REAL

a is complex ext-real real Element of REAL

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

b is complex ext-real real set

c is complex ext-real real set

b + c is complex ext-real real set

q is complex ext-real real Element of REAL

p is complex ext-real real Element of REAL

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

c

b9 is complex ext-real real Element of REAL

[*c

+ (q,c

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

[*(+ (q,c

{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real set

{{}} is non empty set

o is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

o + b is complex ext-real real set

a + b is complex ext-real real set

q is complex ext-real real Element of REAL

p is complex ext-real real Element of REAL

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

c is complex ext-real real Element of REAL

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

c

b9 is Element of REAL+

c

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+

c

b9 is Element of REAL+

c

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

c

[0,c

b9 is Element of REAL+

b9 - c

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

a9 -' c

a9 -' b99 is Element of REAL+

b9 -' c

b99 -' a9 is Element of REAL+

[0,(b99 -' a9)] is set

a9 - c

a9 -' c

c

[0,(c

c

b9 is Element of REAL+

[0,b9] is set

c

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+

c

c

c99 -' a99 is Element of REAL+

c

b99 is Element of REAL+

a9 is Element of REAL+

a99 -' c99 is Element of REAL+

[0,(a99 -' c99)] is set

c

c

a99 -' c

b99 is Element of REAL+

a9 is Element of REAL+

[0,(a99 -' c

c

[0,c

b9 is Element of REAL+

[0,b9] is set

c

[0,(c

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

b9 -' c99 is Element of REAL+

[0,(b9 -' c99)] is set

c

[0,c

b9 is Element of REAL+

[0,b9] is set

c

[0,(c

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+

c

o is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

o + b is complex ext-real real set

c is complex ext-real real set

a + c is complex ext-real real set

a + b is complex ext-real real set

o is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

o - b is complex ext-real real set

a - b is complex ext-real real set

- b is complex ext-real real set

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

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

o is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

o + b is complex ext-real real set

c is complex ext-real real set

a + c is complex ext-real real set

q is complex ext-real real set

p is complex ext-real real set

c

q + c

b9 is complex ext-real real set

p + b9 is complex ext-real real set

b9 + q is complex ext-real real set

(q + c

q + b9 is complex ext-real real set

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

o is complex ext-real real set

a is complex ext-real real set

a + o is complex ext-real real set

a + 0 is complex ext-real real set

o is complex ext-real real set

o + 1 is complex ext-real real set

o + 0 is complex ext-real real set

o is complex ext-real real set

o - 1 is complex ext-real real set

- 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real set

o + (- 0) 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 is complex ext-real real set

a is complex ext-real real set

a + 1 is complex ext-real real set

b is complex ext-real real set

o + 1 is complex ext-real real set

b is complex ext-real real set

o is complex ext-real real set

a is complex ext-real real set

o + a is complex ext-real real set

b is complex ext-real real set

b + a is complex ext-real real set

- a is complex ext-real real set

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

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

o is complex ext-real real set

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

b is complex ext-real real set

o + 0 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 is complex ext-real real set

a + 0 is complex ext-real real set

o is complex ext-real real Element of REAL

a is complex ext-real real Element of REAL

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

b is complex ext-real real set

c is complex ext-real real set

b * c is complex ext-real real set

q is complex ext-real real Element of REAL

p is complex ext-real real Element of REAL

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

c

b9 is complex ext-real real Element of REAL

[*c

* (q,c

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

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

+ ((* (q,c

* (q,b9) is complex ext-real real Element of REAL

* (p,c

+ ((* (q,b9)),(* (p,c

[*(+ ((* (q,c

opp p is complex ext-real real Element of REAL

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

+ ((* (q,c

a is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

a * c is complex ext-real real set

b * c is complex ext-real real set

o is Element of REAL+

p is complex ext-real real Element of REAL

c

* (p,c

q is complex ext-real real Element of REAL

* (q,c

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 is complex ext-real real set

b is complex ext-real real set

b * a is complex ext-real real set

c is complex ext-real real set

c * a is complex ext-real real set

a " is complex ext-real real set

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

b * 1 is complex ext-real real set

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

c * 1 is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a + b is complex ext-real real set

2 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real Element of NAT

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

c is complex ext-real real set

1 * a 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 * a is complex ext-real real set

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

1 * b is complex ext-real real set

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

2 * b is complex ext-real real set

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

a is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

a + c is complex ext-real real set

b + c is complex ext-real real set

q is complex ext-real real set

c

q + c

p is complex ext-real real set

p + c

a is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

q is complex ext-real real set

a + c is complex ext-real real set

b + q is complex ext-real real set

b is complex ext-real real set

a is complex ext-real real set

c is complex ext-real real set

q is complex ext-real real set

b + q is complex ext-real real set

a + c 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

- b is complex ext-real real set

a - b is complex ext-real real set

b - b is complex ext-real real set

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

0 - a 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

- 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

c is complex ext-real real set

a - c is complex ext-real real set

b - c is complex ext-real real set

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

a is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

c - b is complex ext-real real set

c - a is complex ext-real real set

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

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

a - c is complex ext-real real set

b - c is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a + b is complex ext-real real set

c is complex ext-real real set

c - b is complex ext-real real set

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

a is complex ext-real real set

b is complex ext-real real set

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) + c is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a - b is complex ext-real real set

c is complex ext-real real set

b + c is complex ext-real real set

c + b is complex ext-real real set

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

a is complex ext-real real set

b is complex ext-real real set

a - b is complex ext-real real set

c is complex ext-real real set

b + c is complex ext-real real set

- b is complex ext-real real set

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

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

a is complex ext-real real set

b is complex ext-real real set

b - a is complex ext-real real set

c is complex ext-real real set

b - c is complex ext-real real set

a + c is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a - b is complex ext-real real set

c is complex ext-real real set

a - c is complex ext-real real set

c + b is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

b - c is complex ext-real real set

q is complex ext-real real set

a - q is complex ext-real real set

- q is complex ext-real real set

- c is complex ext-real real set

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

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

a is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

b - c is complex ext-real real set

q is complex ext-real real set

a - q is complex ext-real real set

- q is complex ext-real real set

- c is complex ext-real real set

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

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

a is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

b - c is complex ext-real real set

q is complex ext-real real set

a - q is complex ext-real real set

q - a is complex ext-real real set

c - b is complex ext-real real set

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

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

a is complex ext-real real set

b is complex ext-real real set

a + b is complex ext-real real set

c is complex ext-real real set

a - c is complex ext-real real set

q is complex ext-real real set

c + q is complex ext-real real set

q - b 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 is complex ext-real real set

b is complex ext-real real set

a - b is complex ext-real real set

c is complex ext-real real set

a - c is complex ext-real real set

q is complex ext-real real set

c - q is complex ext-real real set

b - q is complex ext-real real set

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

a + q is complex ext-real real set

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

c + b is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a - b is complex ext-real real set

c is complex ext-real real set

c - a is complex ext-real real set

q is complex ext-real real set

c - q is complex ext-real real set

q - b is complex ext-real real set

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

a + q is complex ext-real real set

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

c + b is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a - b is complex ext-real real set

b - a is complex ext-real real set

c is complex ext-real real set

q is complex ext-real real set

c - q is complex ext-real real set

q - c is complex ext-real real set

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

a + q is complex ext-real real set

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

c + b is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a + b is complex ext-real real set

c is complex ext-real real set

c - b is complex ext-real real set

q is complex ext-real real set

c

p is complex ext-real real set

c

q + p is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

b + c is complex ext-real real set

a - b is complex ext-real real set

q is complex ext-real real set

p is complex ext-real real set

q - p is complex ext-real real set

c

p + c

a is complex ext-real real set

b is complex ext-real real set

a + b is complex ext-real real set

c is complex ext-real real set

a - c is complex ext-real real set

q is complex ext-real real set

c + q is complex ext-real real set

q - b is complex ext-real real set

b + a 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 is complex ext-real real set

b is complex ext-real real set

a + b is complex ext-real real set

c is complex ext-real real set

c - b is complex ext-real real set

q is complex ext-real real set

c - q is complex ext-real real set

a + q 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 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 is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a - b is complex ext-real real set

c is complex ext-real real set

c + b is complex ext-real real set

q is complex ext-real real set

c + q is complex ext-real real set

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

q + c is complex ext-real real set

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

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

q + c 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

q is complex ext-real real set

- q is complex ext-real real set

c is complex ext-real real set

- c is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

b - a is complex ext-real real set

a + 0 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

- b is complex ext-real real set

a + b is complex ext-real real set

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

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

a is complex ext-real real set

b is complex ext-real real set

b - a is complex ext-real real set

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

- b is complex ext-real real set

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

a + b is complex ext-real real set

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

a is complex ext-real real set

b is complex ext-real real set

a + b is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a + b is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

b + a is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a + b is complex ext-real real set

0 + b is complex ext-real real set

b + a is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a - b is complex ext-real real set

0 + b is complex ext-real real set

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

a is complex ext-real real set

b is complex ext-real real set

a + b is complex ext-real real set

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

b - a is complex ext-real real set

- a is complex ext-real real set

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

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

b - a is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a + b is complex ext-real real set

b + a is complex ext-real real set

0 + b is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a + b is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a + b is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

b + a is complex ext-real real set

c is complex ext-real real set

a + b is complex ext-real real set

0 + c is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

b + a is complex ext-real real set

c is complex ext-real real set

0 + c is complex ext-real real set

a + b is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

b + a is complex ext-real real set

c is complex ext-real real set

0 + c is complex ext-real real set

a + b is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

a + c is complex ext-real real set

b + 0 is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

a + c is complex ext-real real set

b + 0 is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

a + c is complex ext-real real set

b + 0 is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

b * a is complex ext-real real set

c is complex ext-real real set

c * a is complex ext-real real set

- 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

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

a is complex ext-real real set

b is complex ext-real real set

b / a is complex ext-real real set

c is complex ext-real real set

c / a is complex ext-real real set

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

a is complex ext-real real set

b is complex ext-real real set

b / a is complex ext-real real set

c is complex ext-real real set

c / a is complex ext-real real set

a " is complex ext-real real set

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

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

2 is non empty epsilon-transitive epsilon-connected ordinal natural complex ext-real positive non negative real Element of NAT

a is complex ext-real real set

a / 2 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

a is complex ext-real real set

b is complex ext-real real set

a - b 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 is complex ext-real real set

b is complex ext-real real set

b - a 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

a is complex ext-real real set

b is complex ext-real real set

b - a is complex ext-real real set

b - 0 is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

b - a is complex ext-real real set

b + 0 is complex ext-real real set

- a is complex ext-real real set

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

a is complex ext-real real set

b is complex ext-real real set

b - a is complex ext-real real set

b + a is complex ext-real real set

0 + b is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

b - a is complex ext-real real set

0 + b is complex ext-real real set

b + a is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a - b is complex ext-real real set

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

0 + b is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

b - a is complex ext-real real set

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

b is complex ext-real real set

a is complex ext-real real set

b - a is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

b - a is complex ext-real real set

c is complex ext-real real set

a + c is complex ext-real real set

b + 0 is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

c - a is complex ext-real real set

b + a is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

c - a is complex ext-real real set

b + a is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

c - a is complex ext-real real set

a + b is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a - b is complex ext-real real set

b - a is complex ext-real real set

0 + a is complex ext-real real set

0 + b is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

b - a 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 is complex ext-real real set

b is complex ext-real real set

a - b 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

a 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 is complex ext-real real set

- b is complex ext-real real set

a + b is complex ext-real real set

(- b) + 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 + b is complex ext-real real set

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

b + a 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 + b is complex ext-real real set

(- b) + 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

b + a is complex ext-real real set

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

a is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

b * c is complex ext-real real set

a * c is complex ext-real real set

- 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 * c) is complex ext-real real set

a is complex ext-real real set

a * a is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

a * c is complex ext-real real set

b * c is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

b * c is complex ext-real real set

a * c is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

a * c is complex ext-real real set

q is complex ext-real real set

b * q is complex ext-real real set

b * c is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

a * c is complex ext-real real set

q is complex ext-real real set

b * q is complex ext-real real set

- c is complex ext-real real set

- q is complex ext-real real set

- a is complex ext-real real set

- b is complex ext-real real set

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

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

a is complex ext-real real set

c is complex ext-real real set

b is complex ext-real real set

c * a is complex ext-real real set

b * a is complex ext-real real set

a is complex ext-real real set

c is complex ext-real real set

b is complex ext-real real set

b * a is complex ext-real real set

c * a is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

a * c is complex ext-real real set

q is complex ext-real real set

b * q is complex ext-real real set

a * q is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

q 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

a is complex ext-real real set

b is complex ext-real real set

b / a is complex ext-real real set

c is complex ext-real real set

c / a is complex ext-real real set

- 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

a is complex ext-real real set

b is complex ext-real real set

b / a is complex ext-real real set

c is complex ext-real real set

c / a is complex ext-real real set

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

a is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

b / a is complex ext-real real set

c / a is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

c / a is complex ext-real real set

b / a is complex ext-real real set

a is complex ext-real real set

c is complex ext-real real set

b is complex ext-real real set

c / a is complex ext-real real set

b / a is complex ext-real real set

a is complex ext-real real set

c is complex ext-real real set

b is complex ext-real real set

b / a is complex ext-real real set

c / a is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a / b is complex ext-real real set

c is complex ext-real real set

a / c is complex ext-real real set

c " is complex ext-real real set

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

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

b " 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

a 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

1 / b 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

a is complex ext-real real set

b is complex ext-real real set

b * a is complex ext-real real set

c is complex ext-real real set

c / a is complex ext-real real set

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

a is complex ext-real real set

b is complex ext-real real set

b * a is complex ext-real real set

c is complex ext-real real set

c / a is complex ext-real real set

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

a is complex ext-real real set

b is complex ext-real real set

b / a is complex ext-real real set

c is complex ext-real real set

c * a is complex ext-real real set

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

a is complex ext-real real set

b is complex ext-real real set

b / a is complex ext-real real set

c is complex ext-real real set

c * a is complex ext-real real set

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

a is complex ext-real real set

b is complex ext-real real set

b * a is complex ext-real real set

c is complex ext-real real set

c / a is complex ext-real real set

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

a is complex ext-real real set

b is complex ext-real real set

b * a is complex ext-real real set

c is complex ext-real real set

c / a is complex ext-real real set

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

a is complex ext-real real set

b is complex ext-real real set

b / a is complex ext-real real set

c is complex ext-real real set

c * a is complex ext-real real set

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

a is complex ext-real real set

b is complex ext-real real set

b / a is complex ext-real real set

c is complex ext-real real set

c * a is complex ext-real real set

(c * a) / a 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

b " 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 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 * (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

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

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

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

a 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

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

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

a 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

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

(a ") " 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

b " 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

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 ") " 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

b " is complex ext-real real set

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

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

b is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural complex ext-real non positive non negative real set

a is complex ext-real real set

b * a 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

b - a is complex ext-real real set

b + a is complex ext-real real set

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

b + 0 is complex ext-real real set

0 - a is complex ext-real real set

a + 0 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

b - a is complex ext-real real set

b + a is complex ext-real real set

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

a + 0 is complex ext-real real set

b + 0 is complex ext-real real set

0 - a is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a - b is complex ext-real real set

a + b is complex ext-real real set

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

- b is complex ext-real real set

0 + 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

0 - b is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a * b is complex ext-real real set

c is complex ext-real real set

q is complex ext-real real set

c * q is complex ext-real real set

a * q is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a * b is complex ext-real real set

c is complex ext-real real set

q is complex ext-real real set

c * q is complex ext-real real set

a * q is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a * b is complex ext-real real set

c is complex ext-real real set

q is complex ext-real real set

c * q is complex ext-real real set

a * q is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a / b is complex ext-real real set

c is complex ext-real real set

a / c is complex ext-real real set

c " is complex ext-real real set

b " is complex ext-real real set

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

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

a is complex ext-real real set

b is complex ext-real real set

a / b is complex ext-real real set

c is complex ext-real real set

a / c is complex ext-real real set

b " is complex ext-real real set

c " is complex ext-real real set

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

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

a is complex ext-real real set

b is complex ext-real real set

a / b is complex ext-real real set

c is complex ext-real real set

a / c is complex ext-real real set

c " is complex ext-real real set

b " is complex ext-real real set

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

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

a is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

c * b is complex ext-real real set

c / a is complex ext-real real set

q is complex ext-real real set

q * a is complex ext-real real set

q / 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

a is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

c * b is complex ext-real real set

c / a is complex ext-real real set

q is complex ext-real real set

q * a is complex ext-real real set

q / 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

a is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

c * b is complex ext-real real set

c / a is complex ext-real real set

q is complex ext-real real set

q * a is complex ext-real real set

q / 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

a is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

c * b is complex ext-real real set

c / a is complex ext-real real set

q is complex ext-real real set

q * a is complex ext-real real set

q / 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

a is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

c * b is complex ext-real real set

c / a is complex ext-real real set

q is complex ext-real real set

q * a is complex ext-real real set

q / 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

a is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

c * b is complex ext-real real set

c / a is complex ext-real real set

q is complex ext-real real set

q * a is complex ext-real real set

q / 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

a is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

c * b is complex ext-real real set

c / a is complex ext-real real set

q is complex ext-real real set

q * a is complex ext-real real set

q / 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

a is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

c * b is complex ext-real real set

c / a is complex ext-real real set

q is complex ext-real real set

q * a is complex ext-real real set

q / 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

a is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

c * a is complex ext-real real set

c * b is complex ext-real real set

q is complex ext-real real set

q / b is complex ext-real real set

q / 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

a is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

c * a is complex ext-real real set

c * b is complex ext-real real set

q is complex ext-real real set

q / b is complex ext-real real set

q / 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

a is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

c / b is complex ext-real real set

c / a is complex ext-real real set

q is complex ext-real real set

q * a is complex ext-real real set

q * b 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 is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

c / b is complex ext-real real set

c / a is complex ext-real real set

q is complex ext-real real set

q * a is complex ext-real real set

q * b 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 is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

c * a is complex ext-real real set

c * b is complex ext-real real set

q is complex ext-real real set

q / b is complex ext-real real set

q / 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

a is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

c * a is complex ext-real real set

c * b is complex ext-real real set

q is complex ext-real real set

q / b is complex ext-real real set

q / 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

a is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

c / b is complex ext-real real set

c / a is complex ext-real real set

q is complex ext-real real set

q * a is complex ext-real real set

q * b 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 is complex ext-real real set

b is complex ext-real real set

c is complex ext-real real set

c / b is complex ext-real real set

c / a is complex ext-real real set

q is complex ext-real real set

q * a is complex ext-real real set

q * b 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 is complex ext-real real set

b is complex ext-real real set

b / a is complex ext-real real set

c is complex ext-real real set

b / c is complex ext-real real set

c " is complex ext-real real set

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

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

a " 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

a is complex ext-real real set

b is complex ext-real real set

a / b is complex ext-real real set

c is complex ext-real real set

a / c is complex ext-real real set

b " is complex ext-real real set

c " is complex ext-real real set

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

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

a is complex ext-real real set

b is complex ext-real real set

a / b is complex ext-real real set

c is complex ext-real real set

a / c is complex ext-real real set

c " is complex ext-real real set

b " is complex ext-real real set

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

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

a is complex ext-real real set

b is complex ext-real real set

a / b is complex ext-real real set

c is complex ext-real real set

a / c is complex ext-real real set

b " is complex ext-real real set

c " is complex ext-real real set

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

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

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

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

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

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 * b is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a * b is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a * b is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a * b is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a * b is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a * b is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a * b is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a * b is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a * b is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a / b is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a / b is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a / b is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a / b is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a / b is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a / b is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a / b is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

b / a is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a / b is complex ext-real real set

b " is complex ext-real real set

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

a is complex ext-real real set

b is complex ext-real real set

a / b is complex ext-real real set

b " is complex ext-real real set

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

a is complex ext-real real set

b is complex ext-real real set

b + 1 is complex ext-real real set

a - 1 is complex ext-real real set

b - 1 is complex ext-real real set

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

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

a is complex ext-real real set

a - 1 is complex ext-real real set

a + 0 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

a is complex ext-real real set

a - 1 is complex ext-real real set

b is complex ext-real real set

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

a is complex ext-real real set

1 + a is complex ext-real real set

a + 1 is complex ext-real real set

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

a is complex ext-real real set

1 - a is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a * b is complex ext-real real set

b " is complex ext-real real set

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

a is complex ext-real real set

b is complex ext-real real set

a * b is complex ext-real real set

a * 1 is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a * b is complex ext-real real set

a * 1 is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a * b is complex ext-real real set

a * 1 is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a * b is complex ext-real real set

a * 1 is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a * b is complex ext-real real set

a * 1 is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real set

a * b is complex ext-real real set

a * 1 is complex ext-real real set

a is complex ext-real real set

b is complex ext-real real