:: MEMBER_1 semantic presentation

K13(REAL) is set

K14(COMPLEX,COMPLEX) is set
K13(K14(COMPLEX,COMPLEX)) is set
K14(K14(COMPLEX,COMPLEX),COMPLEX) is set
K13(K14(K14(COMPLEX,COMPLEX),COMPLEX)) is set
K14(REAL,REAL) is set
K13(K14(REAL,REAL)) is set
K14(K14(REAL,REAL),REAL) is set
K13(K14(K14(REAL,REAL),REAL)) is set
K14(RAT,RAT) is set
K13(K14(RAT,RAT)) is set
K14(K14(RAT,RAT),RAT) is set
K13(K14(K14(RAT,RAT),RAT)) is set
K14(INT,INT) is set
K13(K14(INT,INT)) is set
K14(K14(INT,INT),INT) is set
K13(K14(K14(INT,INT),INT)) is set
K14(NAT,NAT) is set
K14(K14(NAT,NAT),NAT) is set
K13(K14(K14(NAT,NAT),NAT)) is set

+infty is non real set
-infty is non real set

- A is ext-real set
A " is ext-real set

A * B is ext-real set
A is complex set
B is complex set
a is complex set
z is complex set
{A,B,a,z} is set
c2 is set
A is ext-real set
B is ext-real set
a is ext-real set
z is ext-real set
{A,B,a,z} is set
c2 is set

{ (b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set
B is set

(a) is ext-real Element of ExtREAL

{ (b1) where b1 is ext-real Element of ExtREAL : b1 in a } is set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in B } is set
z is ext-real set
- z is ext-real set
- (- z) is ext-real set
z is set
c2 is ext-real Element of ExtREAL
(c2) is ext-real Element of ExtREAL
w3 is ext-real Element of ExtREAL
(w3) is ext-real Element of ExtREAL

(A) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set
B is ext-real set
- B is ext-real set
- (- B) is ext-real set

(a) is ext-real Element of ExtREAL

(A) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set
B is ext-real set
- B is ext-real set
- (- B) is ext-real set

(A) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set
the ext-real Element of (A) is ext-real Element of (A)

(B) is ext-real Element of ExtREAL
A is non empty ext-real-membered set
(A) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set
the ext-real Element of A is ext-real Element of A
- the ext-real Element of A is ext-real set

(A) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set

(B) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in B } is set
a is ext-real set
- a is ext-real set

(A) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set

(B) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in B } is set
((A)) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in (A) } is set
((B)) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in (B) } is set

(A) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set

(B) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in B } is set

(A) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set

((A \/ B)) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in A \/ B } is set
(B) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in B } is set
(A) \/ (B) is ext-real-membered set
a is ext-real set
- a is ext-real set

(A) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set

((A /\ B)) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in A /\ B } is set
(B) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in B } is set
(A) /\ (B) is ext-real-membered set
a is ext-real set
- a is ext-real set

(A) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set

A \ B is ext-real-membered Element of K13(A)
K13(A) is set
((A \ B)) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in A \ B } is set
(B) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in B } is set
(A) \ (B) is ext-real-membered Element of K13((A))
K13((A)) is set
a is ext-real set
- a is ext-real set

(A) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set

(A \ B) \/ (B \ A) is ext-real-membered set
((A \+\ B)) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in A \+\ B } is set
(B) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in B } is set
(A) \+\ (B) is ext-real-membered set
(A) \ (B) is ext-real-membered set
(B) \ (A) is ext-real-membered set
((A) \ (B)) \/ ((B) \ (A)) is ext-real-membered set
A \ B is ext-real-membered Element of K13(A)
K13(A) is set
((A \ B)) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in A \ B } is set
B \ A is ext-real-membered Element of K13(B)
K13(B) is set
((B \ A)) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in B \ A } is set
((A \ B)) \/ ((B \ A)) is ext-real-membered set
(A) \ (B) is ext-real-membered Element of K13((A))
K13((A)) is set
((A) \ (B)) \/ ((B \ A)) is ext-real-membered set
A is ext-real set
{A} is non empty ext-real-membered set
({A}) is non empty ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in {A} } is set
- A is ext-real set
{(- A)} is non empty ext-real-membered set
B is ext-real set

(a) is ext-real Element of ExtREAL
A is ext-real set
- A is ext-real set
B is ext-real set
{A,B} is non empty ext-real-membered set
({A,B}) is non empty ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in {A,B} } is set
- B is ext-real set
{(- A),(- B)} is non empty ext-real-membered set
{A} is non empty ext-real-membered set
{B} is non empty ext-real-membered set
{A} \/ {B} is non empty ext-real-membered set
(({A} \/ {B})) is non empty ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in {A} \/ {B} } is set
({A}) is non empty ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in {A} } is set
({B}) is non empty ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in {B} } is set
({A}) \/ ({B}) is non empty ext-real-membered set
{(- A)} is non empty ext-real-membered set
{(- A)} \/ ({B}) is non empty ext-real-membered set
{(- B)} is non empty ext-real-membered set
{(- A)} \/ {(- B)} is non empty ext-real-membered set

{ (- b1) where b1 is complex Element of COMPLEX : b1 in A } is set
B is set

{ (- b1) where b1 is complex Element of COMPLEX : b1 in B } is set

{ (- b1) where b1 is complex Element of COMPLEX : b1 in a } is set
z is complex set

- (- z) is complex Element of COMPLEX
z is set
c2 is complex Element of COMPLEX
- c2 is complex Element of COMPLEX
w3 is complex Element of COMPLEX
- w3 is complex Element of COMPLEX

(A) is complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in A } is set
B is complex set

(A) is complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in A } is set
B is complex set

- (- B) is complex Element of COMPLEX

(A) is complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in A } is set
the complex Element of (A) is complex Element of (A)

A is non empty complex-membered set
(A) is complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in A } is set
the complex Element of A is complex Element of A
- the complex Element of A is complex Element of COMPLEX

(A) is complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in A } is set
B is set

{ (- b1) where b1 is complex Element of COMPLEX : b1 in A } is set
B is set

{ (- b1) where b1 is complex Element of COMPLEX : b1 in A } is set
B is set

{ (- b1) where b1 is complex Element of COMPLEX : b1 in A } is set
(B) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in B } is set
a is ext-real set

(z) is ext-real Element of ExtREAL

- a is ext-real set
(A) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set

(A) is complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in A } is set

(B) is complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in B } is set
a is complex set

(A) is complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in A } is set

(B) is complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in B } is set
((A)) is complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in (A) } is set
((B)) is complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in (B) } is set

(A) is complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in A } is set

(B) is complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in B } is set

(A) is complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in A } is set

((A \/ B)) is complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in A \/ B } is set
(B) is complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in B } is set
(A) \/ (B) is complex-membered set
a is complex set

(A) is complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in A } is set

((A /\ B)) is complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in A /\ B } is set
(B) is complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in B } is set
(A) /\ (B) is complex-membered set
a is complex set

(A) is complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in A } is set

A \ B is complex-membered Element of K13(A)
K13(A) is set
((A \ B)) is complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in A \ B } is set
(B) is complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in B } is set
(A) \ (B) is complex-membered Element of K13((A))
K13((A)) is set
a is complex set

(A) is complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in A } is set

(A \ B) \/ (B \ A) is complex-membered set
((A \+\ B)) is complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in A \+\ B } is set
(B) is complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in B } is set
(A) \+\ (B) is complex-membered set
(A) \ (B) is complex-membered set
(B) \ (A) is complex-membered set
((A) \ (B)) \/ ((B) \ (A)) is complex-membered set
A \ B is complex-membered Element of K13(A)
K13(A) is set
((A \ B)) is complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in A \ B } is set
B \ A is complex-membered Element of K13(B)
K13(B) is set
((B \ A)) is complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in B \ A } is set
((A \ B)) \/ ((B \ A)) is complex-membered set
(A) \ (B) is complex-membered Element of K13((A))
K13((A)) is set
((A) \ (B)) \/ ((B \ A)) is complex-membered set
A is complex set
{A} is non empty complex-membered set
({A}) is non empty complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in {A} } is set

{(- A)} is non empty complex-membered set
B is complex set

A is complex set

B is complex set
{A,B} is non empty complex-membered set
({A,B}) is non empty complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in {A,B} } is set

{(- A),(- B)} is non empty complex-membered set
{A} is non empty complex-membered set
{B} is non empty complex-membered set
{A} \/ {B} is non empty complex-membered set
(({A} \/ {B})) is non empty complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in {A} \/ {B} } is set
({A}) is non empty complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in {A} } is set
({B}) is non empty complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in {B} } is set
({A}) \/ ({B}) is non empty complex-membered set
{(- A)} is non empty complex-membered set
{(- A)} \/ ({B}) is non empty complex-membered set
{(- B)} is non empty complex-membered set
{(- A)} \/ {(- B)} is non empty complex-membered set

{ (b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set
B is set

(a) is ext-real Element of ExtREAL

(A) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set
B is ext-real set
B " is ext-real set

(A) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set
the ext-real Element of (A) is ext-real Element of (A)

(B) is ext-real Element of ExtREAL
A is non empty ext-real-membered set
(A) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set
the ext-real Element of A is ext-real Element of A
the ext-real Element of A " is ext-real set

(A) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set

(B) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in B } is set
a is ext-real set

(z) is ext-real Element of ExtREAL

(A) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set

((A \/ B)) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in A \/ B } is set
(B) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in B } is set
(A) \/ (B) is ext-real-membered set
a is ext-real set

(z) is ext-real Element of ExtREAL

(z) is ext-real Element of ExtREAL

(z) is ext-real Element of ExtREAL

(A) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set

((A /\ B)) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in A /\ B } is set
(B) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in B } is set
(A) /\ (B) is ext-real-membered set
a is ext-real set

(z) is ext-real Element of ExtREAL

(A) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set
((A)) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in (A) } is set
(A) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set
((A)) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in (A) } is set
B is ext-real set
- B is ext-real set

(a) is ext-real Element of ExtREAL
(a) is ext-real Element of ExtREAL
((a)) is ext-real Element of ExtREAL
((a)) is ext-real Element of ExtREAL

(a) is ext-real Element of ExtREAL
(a) is ext-real Element of ExtREAL
((a)) is ext-real Element of ExtREAL
((a)) is ext-real Element of ExtREAL
A is ext-real set
{A} is non empty ext-real-membered set
({A}) is non empty ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in {A} } is set
A " is ext-real set
{(A ")} is non empty ext-real-membered set
B is ext-real set

(a) is ext-real Element of ExtREAL
A is ext-real set
A " is ext-real set
B is ext-real set
{A,B} is non empty ext-real-membered set
({A,B}) is non empty ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in {A,B} } is set
B " is ext-real set
{(A "),(B ")} is non empty ext-real-membered set
{A} is non empty ext-real-membered set
{B} is non empty ext-real-membered set
{A} \/ {B} is non empty ext-real-membered set
(({A} \/ {B})) is non empty ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in {A} \/ {B} } is set
({A}) is non empty ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in {A} } is set
({B}) is non empty ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in {B} } is set
({A}) \/ ({B}) is non empty ext-real-membered set
{(A ")} is non empty ext-real-membered set
{(A ")} \/ ({B}) is non empty ext-real-membered set
{(B ")} is non empty ext-real-membered set
{(A ")} \/ {(B ")} is non empty ext-real-membered set

{ (b1 ") where b1 is complex Element of COMPLEX : b1 in A } is set
B is set

{ (b1 ") where b1 is complex Element of COMPLEX : b1 in B } is set

{ (b1 ") where b1 is complex Element of COMPLEX : b1 in a } is set
z is complex set

(z ") " is complex Element of COMPLEX
z is set
c2 is complex Element of COMPLEX
c2 " is complex Element of COMPLEX
w3 is complex Element of COMPLEX
w3 " is complex Element of COMPLEX

(A) is complex-membered set
{ (b1 ") where b1 is complex Element of COMPLEX : b1 in A } is set
B is complex set

(A) is complex-membered set
{ (b1 ") where b1 is complex Element of COMPLEX : b1 in A } is set
B is complex set

(B ") " is complex Element of COMPLEX

(A) is complex-membered set
{ (b1 ") where b1 is complex Element of COMPLEX : b1 in A } is set
the complex Element of (A) is complex Element of (A)

A is non empty complex-membered set
(A) is complex-membered set
{ (b1 ") where b1 is complex Element of COMPLEX : b1 in A } is set
the complex Element of A is complex Element of A
the complex Element of A " is complex Element of COMPLEX

(A) is complex-membered set
{ (b1 ") where b1 is complex Element of COMPLEX : b1 in A } is set
B is set

{ (b1 ") where b1 is complex Element of COMPLEX : b1 in A } is set
B is set

{ (b1 ") where b1 is complex Element of COMPLEX : b1 in A } is set
(B) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in B } is set
a is ext-real set

c2 is ext-real Element of ExtREAL
(c2) is ext-real Element of ExtREAL
w3 is complex set
w3 " is complex Element of COMPLEX

(z) is ext-real Element of ExtREAL
c2 is complex Element of COMPLEX
c2 " is complex Element of COMPLEX
(A) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set

(A) is complex-membered set
{ (b1 ") where b1 is complex Element of COMPLEX : b1 in A } is set

(B) is complex-membered set
{ (b1 ") where b1 is complex Element of COMPLEX : b1 in B } is set
a is complex set

(A) is complex-membered set
{ (b1 ") where b1 is complex Element of COMPLEX : b1 in A } is set

(B) is complex-membered set
{ (b1 ") where b1 is complex Element of COMPLEX : b1 in B } is set
((A)) is complex-membered set
{ (b1 ") where b1 is complex Element of COMPLEX : b1 in (A) } is set
((B)) is complex-membered set
{ (b1 ") where b1 is complex Element of COMPLEX : b1 in (B) } is set

(A) is complex-membered set
{ (b1 ") where b1 is complex Element of COMPLEX : b1 in A } is set

(B) is complex-membered set
{ (b1 ") where b1 is complex Element of COMPLEX : b1 in B } is set

(A) is complex-membered set
{ (b1 ") where b1 is complex Element of COMPLEX : b1 in A } is set

((A \/ B)) is complex-membered set
{ (b1 ") where b1 is complex Element of COMPLEX : b1 in A \/ B } is set
(B) is complex-membered set
{ (b1 ") where b1 is complex Element of COMPLEX : b1 in B } is set
(A) \/ (B) is complex-membered set
a is complex set

(A) is complex-membered set
{ (b1 ") where b1 is complex Element of COMPLEX : b1 in A } is set

((A /\ B)) is complex-membered set
{ (b1 ") where b1 is complex Element of COMPLEX : b1 in A /\ B } is set
(B) is complex-membered set
{ (b1 ") where b1 is complex Element of COMPLEX : b1 in B } is set
(A) /\ (B) is complex-membered set
a is complex set

(A) is complex-membered set
{ (b1 ") where b1 is complex Element of COMPLEX : b1 in A } is set

A \ B is complex-membered Element of K13(A)
K13(A) is set
((A \ B)) is complex-membered set
{ (b1 ") where b1 is complex Element of COMPLEX : b1 in A \ B } is set
(B) is complex-membered set
{ (b1 ") where b1 is complex Element of COMPLEX : b1 in B } is set
(A) \ (B) is complex-membered Element of K13((A))
K13((A)) is set
a is complex set

(A) is complex-membered set
{ (b1 ") where b1 is complex Element of COMPLEX : b1 in A } is set

(A \ B) \/ (B \ A) is complex-membered set
((A \+\ B)) is complex-membered set
{ (b1 ") where b1 is complex Element of COMPLEX : b1 in A \+\ B } is set
(B) is complex-membered set
{ (b1 ") where b1 is complex Element of COMPLEX : b1 in B } is set
(A) \+\ (B) is complex-membered set
(A) \ (B) is complex-membered set
(B) \ (A) is complex-membered set
((A) \ (B)) \/ ((B) \ (A)) is complex-membered set
A \ B is complex-membered Element of K13(A)
K13(A) is set
((A \ B)) is complex-membered set
{ (b1 ") where b1 is complex Element of COMPLEX : b1 in A \ B } is set
B \ A is complex-membered Element of K13(B)
K13(B) is set
((B \ A)) is complex-membered set
{ (b1 ") where b1 is complex Element of COMPLEX : b1 in B \ A } is set
((A \ B)) \/ ((B \ A)) is complex-membered set
(A) \ (B) is complex-membered Element of K13((A))
K13((A)) is set
((A) \ (B)) \/ ((B \ A)) is complex-membered set

(A) is complex-membered set
{ (b1 ") where b1 is complex Element of COMPLEX : b1 in A } is set
((A)) is complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in (A) } is set
(A) is complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in A } is set
((A)) is complex-membered set
{ (b1 ") where b1 is complex Element of COMPLEX : b1 in (A) } is set
B is complex set

(- B) " is complex Element of COMPLEX

- (B ") is complex Element of COMPLEX
A is complex set
{A} is non empty complex-membered set
({A}) is non empty complex-membered set
{ (b1 ") where b1 is complex Element of COMPLEX : b1 in {A} } is set

{(A ")} is non empty complex-membered set
B is complex set

A is complex set

B is complex set
{A,B} is non empty complex-membered set
({A,B}) is non empty complex-membered set
{ (b1 ") where b1 is complex Element of COMPLEX : b1 in {A,B} } is set

{(A "),(B ")} is non empty complex-membered set
a is complex set

{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in A & b2 in B ) } is set
a is set

{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in z & b2 in c2 ) } is set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in c2 & b2 in z ) } is set
w3 is set
c3 is ext-real Element of ExtREAL
c2 is ext-real Element of ExtREAL
c3 + c2 is ext-real set
w3 is set
c3 is ext-real Element of ExtREAL
c2 is ext-real Element of ExtREAL
c3 + c2 is ext-real set

(A,B) is set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in A & b2 in B ) } is set
a is ext-real set
z is ext-real set
a + z is ext-real set

(A,B) is set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in A & b2 in B ) } is set
the Element of (A,B) is Element of (A,B)

a + z is ext-real set

{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in B & b2 in A ) } is set
A is non empty ext-real-membered set
B is non empty ext-real-membered set
(A,B) is set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in A & b2 in B ) } is set
the ext-real Element of A is ext-real Element of A
the ext-real Element of B is ext-real Element of B
the ext-real Element of A + the ext-real Element of B is ext-real set

(A,B) is set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in A & b2 in B ) } is set
a is set

c2 is ext-real Element of ExtREAL
z + c2 is ext-real set

(A,a) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in A & b2 in a ) } is set

(B,z) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in B & b2 in z ) } is set
c2 is ext-real set
w3 is ext-real Element of ExtREAL
c3 is ext-real Element of ExtREAL
w3 + c3 is ext-real set

(A,B) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in A & b2 in B ) } is set

(A,(B \/ a)) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in A & b2 in B \/ a ) } is set
(A,a) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in A & b2 in a ) } is set
(A,B) \/ (A,a) is ext-real-membered set
z is ext-real set
c2 is ext-real Element of ExtREAL
w3 is ext-real Element of ExtREAL
c2 + w3 is ext-real set
c2 is ext-real Element of ExtREAL
w3 is ext-real Element of ExtREAL
c2 + w3 is ext-real set
c2 is ext-real Element of ExtREAL
w3 is ext-real Element of ExtREAL
c2 + w3 is ext-real set

(A,B) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in A & b2 in B ) } is set

(A,(B /\ a)) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in A & b2 in B /\ a ) } is set
(A,a) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in A & b2 in a ) } is set
(A,B) /\ (A,a) is ext-real-membered set
z is ext-real set
c2 is ext-real Element of ExtREAL
w3 is ext-real Element of ExtREAL
c2 + w3 is ext-real set
A is ext-real set
{A} is non empty ext-real-membered set
B is ext-real set
{B} is non empty ext-real-membered set
({A},{B}) is non empty ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in {B} ) } is set
A + B is ext-real set
{(A + B)} is non empty ext-real-membered set
a is ext-real set

c2 is ext-real Element of ExtREAL
z + c2 is ext-real set
A is ext-real set
{A} is non empty ext-real-membered set
B is ext-real set
A + B is ext-real set
a is ext-real set
{B,a} is non empty ext-real-membered set
({A},{B,a}) is non empty ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in {B,a} ) } is set
A + a is ext-real set
{(A + B),(A + a)} is non empty ext-real-membered set
{B} is non empty ext-real-membered set
{a} is non empty ext-real-membered set
{B} \/ {a} is non empty ext-real-membered set
({A},({B} \/ {a})) is non empty ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in {B} \/ {a} ) } is set
({A},{B}) is non empty ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in {B} ) } is set
({A},{a}) is non empty ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in {a} ) } is set
({A},{B}) \/ ({A},{a}) is non empty ext-real-membered set
{(A + B)} is non empty ext-real-membered set
{(A + B)} \/ ({A},{a}) is non empty ext-real-membered set
{(A + a)} is non empty ext-real-membered set
{(A + B)} \/ {(A + a)} is non empty ext-real-membered set
A is ext-real set
B is ext-real set
{A,B} is non empty ext-real-membered set
a is ext-real set
A + a is ext-real set
B + a is ext-real set
z is ext-real set
{a,z} is non empty ext-real-membered set
({A,B},{a,z}) is non empty ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A,B} & b2 in {a,z} ) } is set
A + z is ext-real set
B + z is ext-real set
{(A + a),(A + z),(B + a),(B + z)} is ext-real-membered set
{A} is non empty ext-real-membered set
{B} is non empty ext-real-membered set
{A} \/ {B} is non empty ext-real-membered set
(({A} \/ {B}),{a,z}) is non empty ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} \/ {B} & b2 in {a,z} ) } is set
({A},{a,z}) is non empty ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in {a,z} ) } is set
({B},{a,z}) is non empty ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {B} & b2 in {a,z} ) } is set
({A},{a,z}) \/ ({B},{a,z}) is non empty ext-real-membered set
{(A + a),(A + z)} is non empty ext-real-membered set
{(A + a),(A + z)} \/ ({B},{a,z}) is non empty ext-real-membered set
{(B + a),(B + z)} is non empty ext-real-membered set
{(A + a),(A + z)} \/ {(B + a),(B + z)} is non empty ext-real-membered set

{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in A & b2 in B ) } is set
a is set

{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in z & b2 in c2 ) } is set
{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in c2 & b2 in z ) } is set
w3 is set
c3 is complex Element of COMPLEX
c2 is complex Element of COMPLEX
c3 + c2 is complex Element of COMPLEX
w3 is set
c3 is complex Element of COMPLEX
c2 is complex Element of COMPLEX
c3 + c2 is complex Element of COMPLEX

(A,B) is set
{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in A & b2 in B ) } is set
a is complex set
z is complex set
a + z is complex Element of COMPLEX

(A,B) is set
{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in A & b2 in B ) } is set
the Element of (A,B) is Element of (A,B)

a + z is complex Element of COMPLEX

{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in B & b2 in A ) } is set
A is non empty complex-membered set
B is non empty complex-membered set
(A,B) is set
{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in A & b2 in B ) } is set
the complex Element of A is complex Element of A
the complex Element of B is complex Element of B
the complex Element of A + the complex Element of B is complex Element of COMPLEX

(A,B) is set
{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in A & b2 in B ) } is set
a is set

c2 is complex Element of COMPLEX
z + c2 is complex Element of COMPLEX

(A,B) is complex-membered set
{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in A & b2 in B ) } is set
a is set

c2 is complex Element of COMPLEX
z + c2 is complex Element of COMPLEX

{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in A & b2 in B ) } is set
a is set

c2 is complex Element of COMPLEX
z + c2 is complex Element of COMPLEX

{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in A & b2 in B ) } is set
a is set

c2 is complex Element of COMPLEX
z + c2 is complex Element of COMPLEX

{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in A & b2 in B ) } is set
a is set

c2 is complex Element of COMPLEX
z + c2 is complex Element of COMPLEX

{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in A & b2 in B ) } is set
(a,z) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in a & b2 in z ) } is set
c2 is ext-real set
w3 is complex Element of COMPLEX
c3 is complex Element of COMPLEX
w3 + c3 is complex Element of COMPLEX
c2 is ext-real Element of ExtREAL
d2 is ext-real Element of ExtREAL
c2 + d2 is ext-real set
w3 is ext-real Element of ExtREAL
c3 is ext-real Element of ExtREAL
w3 + c3 is ext-real set
c2 is complex Element of COMPLEX
d2 is complex Element of COMPLEX
c2 + d2 is complex Element of COMPLEX
(A,B) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in A & b2 in B ) } is set

(A,a) is complex-membered set
{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in A & b2 in a ) } is set

(B,z) is complex-membered set
{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in B & b2 in z ) } is set
c2 is complex set
w3 is complex Element of COMPLEX
c3 is complex Element of COMPLEX
w3 + c3 is complex Element of COMPLEX

(A,B) is complex-membered set
{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in A & b2 in B ) } is set

(A,(B \/ a)) is complex-membered set
{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in A & b2 in B \/ a ) } is set
(A,a) is complex-membered set
{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in A & b2 in a ) } is set
(A,B) \/ (A,a) is complex-membered set
z is complex set
c2 is complex Element of COMPLEX
w3 is complex Element of COMPLEX
c2 + w3 is complex Element of COMPLEX
c2 is complex Element of COMPLEX
w3 is complex Element of COMPLEX
c2 + w3 is complex Element of COMPLEX
c2 is complex Element of COMPLEX
w3 is complex Element of COMPLEX
c2 + w3 is complex Element of COMPLEX

(A,B) is complex-membered set
{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in A & b2 in B ) } is set

(A,(B /\ a)) is complex-membered set
{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in A & b2 in B /\ a ) } is set
(A,a) is complex-membered set
{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in A & b2 in a ) } is set
(A,B) /\ (A,a) is complex-membered set
z is complex set
c2 is complex Element of COMPLEX
w3 is complex Element of COMPLEX
c2 + w3 is complex Element of COMPLEX

(A,B) is complex-membered set
{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in A & b2 in B ) } is set

((A,B),a) is complex-membered set
{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in (A,B) & b2 in a ) } is set
(B,a) is complex-membered set
{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in B & b2 in a ) } is set
(A,(B,a)) is complex-membered set
{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in A & b2 in (B,a) ) } is set
z is complex set
c2 is complex Element of COMPLEX
w3 is complex Element of COMPLEX
c2 + w3 is complex Element of COMPLEX
c3 is complex Element of COMPLEX
c2 is complex Element of COMPLEX
c3 + c2 is complex Element of COMPLEX
c2 + w3 is complex Element of COMPLEX
c3 + (c2 + w3) is complex Element of COMPLEX
c2 is complex Element of COMPLEX
w3 is complex Element of COMPLEX
c2 + w3 is complex Element of COMPLEX
c3 is complex Element of COMPLEX
c2 is complex Element of COMPLEX
c3 + c2 is complex Element of COMPLEX
c2 + c3 is complex Element of COMPLEX
(c2 + c3) + c2 is complex Element of COMPLEX
A is complex set
{A} is non empty complex-membered set
B is complex set
{B} is non empty complex-membered set
({A},{B}) is non empty complex-membered set
{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {A} & b2 in {B} ) } is set
A + B is complex Element of COMPLEX
{(A + B)} is non empty complex-membered set
a is complex set

c2 is complex Element of COMPLEX
z + c2 is complex Element of COMPLEX
A is complex set
{A} is non empty complex-membered set
B is complex set
A + B is complex Element of COMPLEX
a is complex set
{B,a} is non empty complex-membered set
({A},{B,a}) is non empty complex-membered set
{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {A} & b2 in {B,a} ) } is set
A + a is complex Element of COMPLEX
{(A + B),(A + a)} is non empty complex-membered set
{B} is non empty complex-membered set
{a} is non empty complex-membered set
{B} \/ {a} is non empty complex-membered set
({A},({B} \/ {a})) is non empty complex-membered set
{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {A} & b2 in {B} \/ {a} ) } is set
({A},{B}) is non empty complex-membered set
{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {A} & b2 in {B} ) } is set
({A},{a}) is non empty complex-membered set
{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {A} & b2 in {a} ) } is set
({A},{B}) \/ ({A},{a}) is non empty complex-membered set
{(A + B)} is non empty complex-membered set
{(A + B)} \/ ({A},{a}) is non empty complex-membered set
{(A + a)} is non empty complex-membered set
{(A + B)} \/ {(A + a)} is non empty complex-membered set
A is complex set
B is complex set
{A,B} is non empty complex-membered set
a is complex set
A + a is complex Element of COMPLEX
B + a is complex Element of COMPLEX
z is complex set
{a,z} is non empty complex-membered set
({A,B},{a,z}) is non empty complex-membered set
{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {A,B} & b2 in {a,z} ) } is set
A + z is complex Element of COMPLEX
B + z is complex Element of COMPLEX
{(A + a),(A + z),(B + a),(B + z)} is complex-membered set
{A} is non empty complex-membered set
{B} is non empty complex-membered set
{A} \/ {B} is non empty complex-membered set
(({A} \/ {B}),{a,z}) is non empty complex-membered set
{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {A} \/ {B} & b2 in {a,z} ) } is set
({A},{a,z}) is non empty complex-membered set
{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {A} & b2 in {a,z} ) } is set
({B},{a,z}) is non empty complex-membered set
{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in {B} & b2 in {a,z} ) } is set
({A},{a,z}) \/ ({B},{a,z}) is non empty complex-membered set
{(A + a),(A + z)} is non empty complex-membered set
{(A + a),(A + z)} \/ ({B},{a,z}) is non empty complex-membered set
{(B + a),(B + z)} is non empty complex-membered set
{(A + a),(A + z)} \/ {(B + a),(B + z)} is non empty complex-membered set

(B) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in B } is set
(A,(B)) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in A & b2 in (B) ) } is set

(A,B) is set
(B) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in B } is set
(A,(B)) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in A & b2 in (B) ) } is set
{ (b1 - b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in A & b2 in B ) } is set
a is set

c2 is ext-real Element of ExtREAL
z + c2 is ext-real set
(c2) is ext-real Element of ExtREAL
z - (c2) is ext-real set
- (c2) is ext-real set
z + (- (c2)) is ext-real set
a is set

c2 is ext-real Element of ExtREAL
z - c2 is ext-real set
- c2 is ext-real set
z + (- c2) is ext-real set
(c2) is ext-real Element of ExtREAL

(A,B) is set
(B) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in B } is set
(A,(B)) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in A & b2 in (B) ) } is set
a is ext-real set
z is ext-real set
a - z is ext-real set
- z is ext-real set
a + (- z) is ext-real set
{ (b1 - b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in A & b2 in B ) } is set

(A,B) is set
(B) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in B } is set

{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in A & b2 in (B) ) } is set
(B,A) is set

{ (b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set

{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in B & b2 in (A) ) } is set
A is non empty ext-real-membered set
B is non empty ext-real-membered set
(A,B) is set
(B) is non empty ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in B } is set
(A,(B)) is non empty ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in A & b2 in (B) ) } is set

(A,B) is set
(B) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in B } is set
(A,(B)) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in A & b2 in (B) ) } is set

(A,a) is ext-real-membered set
(a) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in a } is set
(A,(a)) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in A & b2 in (a) ) } is set

(B,z) is ext-real-membered set
(z) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in z } is set
(B,(z)) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in B & b2 in (z) ) } is set
c2 is ext-real set
{ (b1 - b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in A & b2 in a ) } is set
w3 is ext-real Element of ExtREAL
c3 is ext-real Element of ExtREAL
w3 - c3 is ext-real set
- c3 is ext-real set
w3 + (- c3) is ext-real set

(A,B) is ext-real-membered set
(B) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in B } is set
(A,(B)) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in A & b2 in (B) ) } is set

(A,(B \/ a)) is ext-real-membered set
((B \/ a)) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in B \/ a } is set
(A,((B \/ a))) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in A & b2 in ((B \/ a)) ) } is set
(A,a) is ext-real-membered set
(a) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in a } is set
(A,(a)) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in A & b2 in (a) ) } is set
(A,B) \/ (A,a) is ext-real-membered set
(B) \/ (a) is ext-real-membered set
(A,((B) \/ (a))) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in A & b2 in (B) \/ (a) ) } is set

(A,B) is ext-real-membered set
(B) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in B } is set
(A,(B)) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in A & b2 in (B) ) } is set

(A,(B /\ a)) is ext-real-membered set
((B /\ a)) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in B /\ a } is set
(A,((B /\ a))) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in A & b2 in ((B /\ a)) ) } is set
(A,a) is ext-real-membered set
(a) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in a } is set
(A,(a)) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in A & b2 in (a) ) } is set
(A,B) /\ (A,a) is ext-real-membered set
(B) /\ (a) is ext-real-membered set
(A,((B) /\ (a))) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in A & b2 in (B) /\ (a) ) } is set

(A) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set

(A,B) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in A & b2 in B ) } is set
((A,B)) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in (A,B) } is set
(B) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in B } is set
((A),(B)) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in (A) & b2 in (B) ) } is set
a is ext-real set

(z) is ext-real Element of ExtREAL
c2 is ext-real Element of ExtREAL
w3 is ext-real Element of ExtREAL
c2 + w3 is ext-real set
- (c2 + w3) is ext-real set
(c2) is ext-real Element of ExtREAL
(c2) - w3 is ext-real set
- w3 is ext-real set
(c2) + (- w3) is ext-real set
(w3) is ext-real Element of ExtREAL

c2 is ext-real Element of ExtREAL
z + c2 is ext-real set
(z) is ext-real Element of ExtREAL
(c2) is ext-real Element of ExtREAL
- (z + c2) is ext-real set
(z) - c2 is ext-real set
- c2 is ext-real set
(z) + (- c2) is ext-real set
(z) + (c2) is ext-real set

(A,B) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in A & b2 in B ) } is set
((A,B)) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in (A,B) } is set
(A) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set
((A),B) is ext-real-membered set
(B) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in B } is set
((A),(B)) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in (A) & b2 in (B) ) } is set

(A) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set

(A,B) is ext-real-membered set
(B) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in B } is set
(A,(B)) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in A & b2 in (B) ) } is set
((A,B)) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in (A,B) } is set
((A),B) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in (A) & b2 in B ) } is set
((A),(B)) is ext-real-membered set
((B)) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in (B) } is set
((A),((B))) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in (A) & b2 in ((B)) ) } is set
A is ext-real set
{A} is non empty ext-real-membered set
B is ext-real set
{B} is non empty ext-real-membered set
({A},{B}) is non empty ext-real-membered set
({B}) is non empty ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in {B} } is set
({A},({B})) is non empty ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in ({B}) ) } is set
A - B is ext-real set
- B is ext-real set
A + (- B) is ext-real set
{(A - B)} is non empty ext-real-membered set
{(- B)} is non empty ext-real-membered set
({A},{(- B)}) is non empty ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in {(- B)} ) } is set
A is ext-real set
{A} is non empty ext-real-membered set
B is ext-real set
A - B is ext-real set
- B is ext-real set
A + (- B) is ext-real set
a is ext-real set
{B,a} is non empty ext-real-membered set
({A},{B,a}) is non empty ext-real-membered set
({B,a}) is non empty ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in {B,a} } is set
({A},({B,a})) is non empty ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in ({B,a}) ) } is set
A - a is ext-real set
- a is ext-real set
A + (- a) is ext-real set
{(A - B),(A - a)} is non empty ext-real-membered set
{(- B),(- a)} is non empty ext-real-membered set
({A},{(- B),(- a)}) is non empty ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A} & b2 in {(- B),(- a)} ) } is set
A is ext-real set
B is ext-real set
{A,B} is non empty ext-real-membered set
a is ext-real set
{a} is non empty ext-real-membered set
({A,B},{a}) is non empty ext-real-membered set
({a}) is non empty ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in {a} } is set
({A,B},({a})) is non empty ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A,B} & b2 in ({a}) ) } is set
A - a is ext-real set
- a is ext-real set
A + (- a) is ext-real set
B - a is ext-real set
B + (- a) is ext-real set
{(A - a),(B - a)} is non empty ext-real-membered set
{(- a)} is non empty ext-real-membered set
({A,B},{(- a)}) is non empty ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A,B} & b2 in {(- a)} ) } is set
A is ext-real set
B is ext-real set
{A,B} is non empty ext-real-membered set
a is ext-real set
A - a is ext-real set
- a is ext-real set
A + (- a) is ext-real set
B - a is ext-real set
B + (- a) is ext-real set
z is ext-real set
{a,z} is non empty ext-real-membered set
({A,B},{a,z}) is non empty ext-real-membered set
({a,z}) is non empty ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in {a,z} } is set
({A,B},({a,z})) is non empty ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A,B} & b2 in ({a,z}) ) } is set
A - z is ext-real set
- z is ext-real set
A + (- z) is ext-real set
B - z is ext-real set
B + (- z) is ext-real set
{(A - a),(A - z),(B - a),(B - z)} is ext-real-membered set
{(- a),(- z)} is non empty ext-real-membered set
({A,B},{(- a),(- z)}) is non empty ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in {A,B} & b2 in {(- a),(- z)} ) } is set

(B) is complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in B } is set
(A,(B)) is complex-membered set
{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in A & b2 in (B) ) } is set

(A,B) is set
(B) is complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in B } is set
(A,(B)) is complex-membered set
{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in A & b2 in (B) ) } is set
{ (b1 - b2) where b1, b2 is complex Element of COMPLEX : ( b1 in A & b2 in B ) } is set
a is set

c2 is complex Element of COMPLEX
z + c2 is complex Element of COMPLEX
- c2 is complex Element of COMPLEX
z - (- c2) is complex Element of COMPLEX
- (- c2) is complex set
z + (- (- c2)) is complex set
a is set

c2 is complex Element of COMPLEX
z - c2 is complex Element of COMPLEX
- c2 is complex set
z + (- c2) is complex set
- c2 is complex Element of COMPLEX

(A,B) is set
(B) is complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in B } is set
(A,(B)) is complex-membered set
{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in A & b2 in (B) ) } is set
a is complex set
z is complex set
a - z is complex Element of COMPLEX
- z is complex set
a + (- z) is complex set
{ (b1 - b2) where b1, b2 is complex Element of COMPLEX : ( b1 in A & b2 in B ) } is set

(A,B) is set
(B) is complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in B } is set

{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in A & b2 in (B) ) } is set
(B,A) is set

{ (- b1) where b1 is complex Element of COMPLEX : b1 in A } is set

{ (b1) where b1 is ext-real Element of ExtREAL : b1 in A } is set

{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in B & b2 in (A) ) } is set
A is non empty complex-membered set
B is non empty complex-membered set
(A,B) is set
(B) is non empty complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in B } is set
(A,(B)) is non empty complex-membered set
{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in A & b2 in (B) ) } is set

(A,B) is set
(B) is complex-membered set
{ (- b1) where b1 is complex Element of COMPLEX : b1 in B } is set
(A,(B)) is complex-membered set
{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in A & b2 in (B) ) } is set

(A,B) is complex-membered set

{ (- b1) where b1 is complex Element of COMPLEX : b1 in B } is set
(B) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in B } is set

{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in A & b2 in (B) ) } is set
(A,(B)) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in A & b2 in (B) ) } is set

{ (- b1) where b1 is complex Element of COMPLEX : b1 in B } is set
(B) is ext-real-membered set
{ (b1) where b1 is ext-real Element of ExtREAL : b1 in B } is set

{ (b1 + b2) where b1, b2 is complex Element of COMPLEX : ( b1 in A & b2 in (B) ) } is set
(A,(B)) is ext-real-membered set
{ (b1 + b2) where b1, b2 is ext-real Element of ExtREAL : ( b1 in A & b2 in (B) ) } is set