:: SQUARE_1 semantic presentation

REAL is non zero set

NAT is non zero epsilon-transitive epsilon-connected ordinal Element of K6(REAL)

K6(REAL) is set

COMPLEX is non zero set

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

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

{ b

{ b

b is set

eps is complex ext-real real Element of REAL

b is set

eps is complex ext-real real Element of REAL

b is Element of K6(REAL)

eps is Element of K6(REAL)

eps is complex ext-real real set

x is complex ext-real real set

y is complex ext-real real Element of REAL

c

eps is complex ext-real real set

x is complex ext-real real set

y is complex ext-real real set

a is complex ext-real real Element of REAL

b is complex ext-real real Element of REAL

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

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

a is complex ext-real real set

b is complex ext-real real set

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

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

(min (a,b)) + (max (a,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

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

a + b is complex ext-real real set

a + 0 is complex ext-real real set

b + 0 is complex ext-real real set

b + a is complex ext-real real set

a is complex set

a * a is complex set

a is complex set

(a) is set

a * a is complex set

a is complex ext-real real set

(a) is complex set

a * a is complex ext-real real set

a is complex Element of COMPLEX

(a) is complex set

a * a is complex set

a is complex ext-real real Element of REAL

(a) is complex ext-real real set

a * a is complex ext-real real set

a is complex set

(a) is complex set

a * a is complex set

- a is complex set

((- a)) is complex set

(- a) * (- a) is complex set

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

a is complex set

b is complex set

a + b is complex set

((a + b)) is complex set

(a + b) * (a + b) is complex set

(a) is complex set

a * a is complex set

2 * a is complex set

(2 * a) * b is complex set

(a) + ((2 * a) * b) is complex set

(b) is complex set

b * b is complex set

((a) + ((2 * a) * b)) + (b) is complex set

a is complex set

b is complex set

a - b is complex set

- b is complex set

a + (- b) is complex set

((a - b)) is complex set

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

(a) is complex set

a * a is complex set

2 * a is complex set

(2 * a) * b is complex set

(a) - ((2 * a) * b) is complex set

- ((2 * a) * b) is complex set

(a) + (- ((2 * a) * b)) is complex set

(b) is complex set

b * b is complex set

((a) - ((2 * a) * b)) + (b) is complex set

a is complex set

a + 1 is complex set

((a + 1)) is complex set

(a + 1) * (a + 1) is complex set

(a) is complex set

a * a is complex set

2 * a is complex set

(a) + (2 * a) is complex set

((a) + (2 * a)) + 1 is complex set

a is complex set

a - 1 is complex set

- 1 is non zero complex ext-real non positive negative real set

a + (- 1) is complex set

((a - 1)) is complex set

(a - 1) * (a - 1) is complex set

(a) is complex set

a * a is complex set

2 * a is complex set

(a) - (2 * a) is complex set

- (2 * a) is complex set

(a) + (- (2 * a)) is complex set

((a) - (2 * a)) + 1 is complex set

a is complex set

b is complex set

a - b is complex set

- b is complex set

a + (- b) is complex set

a + b is complex set

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

(a) is complex set

a * a is complex set

(b) is complex set

b * b is complex set

(a) - (b) is complex set

- (b) is complex set

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

a is complex set

b is complex set

a * b is complex set

((a * b)) is complex set

(a * b) * (a * b) is complex set

(a) is complex set

a * a is complex set

(b) is complex set

b * b is complex set

(a) * (b) is complex set

a is complex set

(a) is complex set

a * a is complex set

b is complex set

(b) is complex set

b * b is complex set

(a) - (b) is complex set

- (b) is complex set

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

a + b is complex set

1 / (a + b) is complex set

(a + b) " is complex set

1 * ((a + b) ") is complex set

a - b is complex set

- b is complex set

a + (- b) is complex set

(a - b) / ((a) - (b)) is complex set

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

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

1 * (a - b) is complex set

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

(1 * (a - b)) / ((a + b) * (a - b)) is complex set

((a + b) * (a - b)) " is complex set

(1 * (a - b)) * (((a + b) * (a - b)) ") is complex set

a is complex set

(a) is complex set

a * a is complex set

b is complex set

(b) is complex set

b * b is complex set

(a) - (b) is complex set

- (b) is complex set

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

a - b is complex set

- b is complex set

a + (- b) is complex set

1 / (a - b) is complex set

(a - b) " is complex set

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

a + b is complex set

(a + b) / ((a) - (b)) is complex set

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

(a + b) * (((a) - (b)) ") is complex set

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

1 * (a + b) is complex set

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

(1 * (a + b)) / ((a - b) * (a + b)) is complex set

((a - b) * (a + b)) " is complex set

(1 * (a + b)) * (((a - b) * (a + b)) ") is complex set

a 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

(a) is complex ext-real real set

a * a is complex ext-real real set

a * 1 is complex ext-real real set

a is complex ext-real real set

(a) is complex ext-real real set

a * a is complex ext-real real set

a * 1 is complex ext-real real set

a is complex ext-real real set

2 " is non zero complex ext-real positive non negative real set

b is complex ext-real real set

(b) is complex ext-real real set

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

(a) is complex ext-real real set

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

a is complex ext-real real set

(a) is complex ext-real real set

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

a is complex ext-real real set

(a) is complex ext-real real set

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

a + 1 is complex ext-real real set

0 + a is complex ext-real real set

(a) is complex ext-real real set

a * a is complex ext-real real set

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

((a) + a) + (a + 1) 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

b is complex ext-real real set

(b) is complex ext-real real set

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

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

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

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

2 " is non zero complex ext-real positive non negative real set

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

eps is complex ext-real real set

(eps) is complex ext-real real set

eps * eps is complex ext-real real set

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

4 * b is complex ext-real real set

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

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

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

min (eps,((a - (b)) / (4 * b))) is complex ext-real real set

b + (min (eps,((a - (b)) / (4 * b)))) is complex ext-real real set

2 * b is complex ext-real real set

(min (eps,((a - (b)) / (4 * b)))) * (2 * b) is complex ext-real real set

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

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

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

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

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

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

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

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

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

(2 * b) * (min (eps,((a - (b)) / (4 * b)))) is complex ext-real real set

((min (eps,((a - (b)) / (4 * b))))) is complex ext-real real set

(min (eps,((a - (b)) / (4 * b)))) * (min (eps,((a - (b)) / (4 * b)))) is complex ext-real real set

((2 * b) * (min (eps,((a - (b)) / (4 * b))))) + ((min (eps,((a - (b)) / (4 * b))))) is complex ext-real real set

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

((b + (min (eps,((a - (b)) / (4 * b)))))) is complex ext-real real set

(b + (min (eps,((a - (b)) / (4 * b))))) * (b + (min (eps,((a - (b)) / (4 * b))))) is complex ext-real real set

(b) + (((2 * b) * (min (eps,((a - (b)) / (4 * b))))) + ((min (eps,((a - (b)) / (4 * b)))))) 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) + (- a) is complex ext-real real set

2 * b is complex ext-real real set

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

((2 * b) * (min ((((b) - a) / (2 * b)),b))) - 0 is complex ext-real real set

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

((2 * b) * (min ((((b) - a) / (2 * b)),b))) + (- 0) is complex ext-real real set

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

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

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

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

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

b is complex ext-real real set

(b) is complex ext-real real set

b * b is complex ext-real real set

a is complex ext-real real Element of REAL

(a) is complex ext-real real set

(0) is complex ext-real real Element of REAL

(0) is complex ext-real real Element of REAL

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

((0)) is complex ext-real real Element of REAL

(1) is complex ext-real real Element of REAL

(1) is complex ext-real real Element of REAL

1 * 1 is non zero complex ext-real positive non negative real set

((1)) is complex ext-real real Element of REAL

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

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

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

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

(2) is complex ext-real real Element of REAL

(2) is complex ext-real real Element of REAL

2 * 2 is non zero complex ext-real positive non negative real set

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

(4) is complex ext-real real Element of REAL

a 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

a 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

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

(a) is complex ext-real real set

(0) is complex ext-real real Element of REAL

0 * 0 is zero 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

(a) is complex ext-real real set

(0) is complex ext-real real Element of REAL

0 * 0 is zero 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

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

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

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

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

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

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

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

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

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

b " is complex ext-real real set

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

(b) " is complex ext-real real set

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

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

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

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

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

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

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

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

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

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

a 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

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

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

(a) " is complex ext-real real set

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

(0) is complex ext-real real Element of REAL

0 * 0 is zero 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

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

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

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

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

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

1 * a is complex ext-real real set

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

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

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

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

a 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

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

(0) is complex ext-real real Element of REAL

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

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

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

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

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

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

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

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

1 * a is complex ext-real real set

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

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

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

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

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

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

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

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

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

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

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

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

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

(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

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

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

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

- 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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

- (b) is complex ext-real real set

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

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

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

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

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

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

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

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

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

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

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

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

- (a) is complex ext-real real set

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

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

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

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

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

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

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

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

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

a is complex set

(a) is complex set

a * a is complex set

b is complex set

(b) is complex set

b * b is complex set

- b is complex set

a - b is complex set

a + (- b) is complex set

a + b is complex set

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

- 1 is non zero complex ext-real non positive negative real set

a is complex set

(a) is complex set

a * a is complex set

a - 1 is complex set

a + (- 1) is complex set

a + 1 is complex set

(a - 1) * (a + 1) is complex set

a 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

(a) is complex ext-real real set

a * a is complex ext-real real set

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

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

a - 1 is complex ext-real real set

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

a + 1 is complex ext-real real set

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

a is complex ext-real real set

(a) is complex ext-real real set

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

- b is complex ext-real real set

- a is complex ext-real real set

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

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

- a is complex ext-real real set

(a) is complex ext-real real set

a * a is complex ext-real real set

- (- 1) is non zero complex ext-real positive non negative real set

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

a * a is complex ext-real real set

- a is complex ext-real real set

- (- 1) is non zero complex ext-real positive non negative real set

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

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

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

a is complex ext-real real set

(a) is complex ext-real real set

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

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

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

- b is complex ext-real real set

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

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

(a) is complex ext-real real set

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

(a) is complex ext-real real set

a * a is complex ext-real real set

(1) is complex ext-real real Element of REAL

1 * 1 is non zero complex ext-real positive non negative real set

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

- (1) is complex ext-real real set

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

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

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

a - 1 is complex ext-real real set

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

a + 1 is complex ext-real real set

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

a is complex ext-real real set

(a) is complex ext-real real set

a * a is complex ext-real real set

(1) is complex ext-real real Element of REAL

1 * 1 is non zero complex ext-real positive non negative real set

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

- (1) is complex ext-real real set

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

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

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

a - 1 is complex ext-real real set

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

a + 1 is complex ext-real real set

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

a is complex ext-real real set

(a) is complex ext-real real set

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

(1) is complex ext-real real Element of REAL

1 * 1 is non zero complex ext-real positive non negative real set

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

a is complex ext-real real set

(a) is complex ext-real real set

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

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

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

a * a is complex ext-real real set

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

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

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

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

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

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

a is complex ext-real real set

(a) is complex ext-real real set

a * a is complex ext-real real set

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

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

b is complex ext-real real set

- b is complex ext-real real set

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

(b) is complex ext-real real set

b * b is complex ext-real real set

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

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

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

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

1 + 0 is non zero complex ext-real positive non negative real set

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

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

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

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

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

a is complex ext-real real set

(a) is complex ext-real real set

a * a is complex ext-real real set

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

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

b is complex ext-real real set

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

(b) is complex ext-real real set

b * b is complex ext-real real set

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

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

- b is complex ext-real real set

- (- 1) is non zero complex ext-real positive non negative real set

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

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

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

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

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

a * a is complex ext-real real set

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

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

b is complex ext-real real set

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

(b) is complex ext-real real set

b * b is complex ext-real real set

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

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

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

- b is complex ext-real real set

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

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

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

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

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

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

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

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

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

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

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

- a is complex ext-real real set

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

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

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

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

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

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

- (b * ((1 + (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

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

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

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

(a) is complex ext-real real set

a * a is complex ext-real real set

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

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

b * ((1 + (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

a * a is complex ext-real real set

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

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

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

(b) is complex ext-real real set

b * b is complex ext-real real set

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

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

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

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

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

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

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

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

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

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

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

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

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

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

a is complex ext-real real set

(a) is complex ext-real real set

a * a is complex ext-real real set

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

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

b is complex ext-real real set

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

(b) is complex ext-real real set

b * b is complex ext-real real set

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

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

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

b * b is complex ext-real real set

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

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

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

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

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

a + 0 is complex ext-real real set

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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