:: BORSUK_5 semantic presentation

REAL is V128() V129() V130() V134() set

NAT is V128() V129() V130() V131() V132() V133() V134() Element of bool REAL

bool REAL is non empty set

I[01] is TopSpace-like T_0 T_1 T_2 compact V127() pathwise_connected SubSpace of R^1

R^1 is non empty strict TopSpace-like T_0 T_1 T_2 V127() TopStruct

the carrier of I[01] is V128() V129() V130() set

COMPLEX is V128() V134() set

omega is V128() V129() V130() V131() V132() V133() V134() set

bool omega is non empty set

[:NAT,REAL:] is set

bool [:NAT,REAL:] is non empty set

bool (bool REAL) is non empty set

K258() is T_0 T_1 T_2 compact V127() pathwise_connected TopStruct

the carrier of K258() is V128() V129() V130() set

1 is non empty natural complex real ext-real positive non negative V128() V129() V130() V131() V132() V133() integer non irrational Element of NAT

[:1,1:] is non empty set

bool [:1,1:] is non empty set

[:[:1,1:],1:] is non empty set

bool [:[:1,1:],1:] is non empty set

[:[:1,1:],REAL:] is set

bool [:[:1,1:],REAL:] is non empty set

[:REAL,REAL:] is set

[:[:REAL,REAL:],REAL:] is set

bool [:[:REAL,REAL:],REAL:] is non empty set

2 is non empty natural complex real ext-real positive non negative V128() V129() V130() V131() V132() V133() integer non irrational Element of NAT

[:2,2:] is non empty set

[:[:2,2:],REAL:] is set

bool [:[:2,2:],REAL:] is non empty set

RealSpace is non empty strict Reflexive discerning symmetric triangle Discerning V127() MetrStruct

0 is empty natural complex real ext-real non positive non negative V36() V40() V128() V129() V130() V131() V132() V133() V134() integer non irrational Element of NAT

the empty V36() V40() V128() V129() V130() V131() V132() V133() V134() set is empty V36() V40() V128() V129() V130() V131() V132() V133() V134() set

Closed-Interval-TSpace (0,1) is non empty strict TopSpace-like V127() SubSpace of R^1

the carrier of (Closed-Interval-TSpace (0,1)) is non empty V128() V129() V130() set

ExtREAL is V129() set

RAT is V128() V129() V130() V131() V134() set

INT is V128() V129() V130() V131() V132() V134() set

{} is empty V36() V40() V128() V129() V130() V131() V132() V133() V134() set

{{},1} is non empty V36() set

bool NAT is non empty set

[:COMPLEX,COMPLEX:] is set

bool [:COMPLEX,COMPLEX:] is non empty set

[:COMPLEX,REAL:] is set

bool [:COMPLEX,REAL:] is non empty set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set

bool [:REAL,REAL:] is non empty set

[:RAT,RAT:] is set

bool [:RAT,RAT:] is non empty set

[:[:RAT,RAT:],RAT:] is set

bool [:[:RAT,RAT:],RAT:] is non empty set

[:INT,INT:] is set

bool [:INT,INT:] is non empty set

[:[:INT,INT:],INT:] is set

bool [:[:INT,INT:],INT:] is non empty set

[:NAT,NAT:] is set

[:[:NAT,NAT:],NAT:] is set

bool [:[:NAT,NAT:],NAT:] is non empty set

the carrier of RealSpace is non empty V128() V129() V130() set

TopSpaceMetr RealSpace is TopStruct

the carrier of R^1 is non empty V128() V129() V130() set

bool the carrier of R^1 is non empty set

Family_open_set RealSpace is Element of bool (bool the carrier of RealSpace)

bool the carrier of RealSpace is non empty set

bool (bool the carrier of RealSpace) is non empty set

(#) (0,1) is complex real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))

(0,1) (#) is complex real ext-real Element of the carrier of (Closed-Interval-TSpace (0,1))

real_dist is V19() V22([:REAL,REAL:]) V23( REAL ) Function-like V33([:REAL,REAL:], REAL ) Element of bool [:[:REAL,REAL:],REAL:]

MetrStruct(# REAL,real_dist #) is strict MetrStruct

5 is non empty natural complex real ext-real positive non negative V128() V129() V130() V131() V132() V133() integer non irrational Element of NAT

number_e is complex real ext-real set

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

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

K451(-infty,+infty) is set

T is set

F is set

P is set

p2 is set

c

C is set

{T,F,P,p2,c

{T,P,C} is non empty V36() set

{F,p2,c

{T,P,C} \/ {F,p2,c

C is set

C is set

6 is non empty natural complex real ext-real positive non negative V128() V129() V130() V131() V132() V133() integer non irrational Element of NAT

T is set

F is set

P is set

p2 is set

c

C is set

{T,F,P,p2,c

card {T,F,P,p2,c

{T,F,P,p2,c

{C} is non empty V36() set

{T,F,P,p2,c

card {T,F,P,p2,c

5 + 1 is non empty complex real ext-real positive non negative integer non irrational set

7 is non empty natural complex real ext-real positive non negative V128() V129() V130() V131() V132() V133() integer non irrational Element of NAT

T is set

F is set

P is set

p2 is set

c

C is set

C is set

{T,F,P,p2,c

card {T,F,P,p2,c

{T,F,P,p2,c

{C} is non empty V36() set

{T,F,P,p2,c

card {T,F,P,p2,c

6 + 1 is non empty complex real ext-real positive non negative integer non irrational set

T is set

F is set

P is set

{T,F,P} is non empty V36() set

p2 is set

c

C is set

{p2,c

T is set

F is set

P is set

{T,F,P} is non empty V36() set

p2 is set

c

C is set

{p2,c

T is set

F is set

P is set

p2 is set

c

C is set

{T,F,P,p2,c

C is set

{C} is non empty V36() set

T is set

F is set

P is set

p2 is set

c

C is set

C is set

T is set

F is set

P is set

p2 is set

c

C is set

C is set

T is complex real ext-real Element of the carrier of R^1

F is complex real ext-real Element of the carrier of R^1

[.T,F.] is V128() V129() V130() closed Element of bool REAL

P is V128() V129() V130() Element of bool the carrier of R^1

Closed-Interval-TSpace (T,F) is non empty strict TopSpace-like V127() SubSpace of R^1

p2 is non empty V128() V129() V130() Element of bool the carrier of R^1

R^1 | p2 is non empty strict TopSpace-like V127() SubSpace of R^1

the carrier of (R^1 | p2) is non empty V128() V129() V130() set

[: the carrier of I[01], the carrier of R^1:] is set

bool [: the carrier of I[01], the carrier of R^1:] is non empty set

(#) (T,F) is complex real ext-real Element of the carrier of (Closed-Interval-TSpace (T,F))

the carrier of (Closed-Interval-TSpace (T,F)) is non empty V128() V129() V130() set

(T,F) (#) is complex real ext-real Element of the carrier of (Closed-Interval-TSpace (T,F))

L[01] (((#) (T,F)),((T,F) (#))) is V19() V22( the carrier of (Closed-Interval-TSpace (0,1))) V23( the carrier of (Closed-Interval-TSpace (T,F))) Function-like V33( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (T,F))) Element of bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (T,F)):]

[: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (T,F)):] is non empty set

bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (T,F)):] is non empty set

c

C is V19() V22( the carrier of I[01]) V23( the carrier of R^1) Function-like V33( the carrier of I[01], the carrier of R^1) Element of bool [: the carrier of I[01], the carrier of R^1:]

C . 0 is set

C . 1 is set

[: the carrier of I[01], the carrier of (R^1 | p2):] is set

bool [: the carrier of I[01], the carrier of (R^1 | p2):] is non empty set

[.F,T.] is V128() V129() V130() closed Element of bool REAL

P is V128() V129() V130() Element of bool the carrier of R^1

Closed-Interval-TSpace (F,T) is non empty strict TopSpace-like V127() SubSpace of R^1

p2 is non empty V128() V129() V130() Element of bool the carrier of R^1

R^1 | p2 is non empty strict TopSpace-like V127() SubSpace of R^1

the carrier of (R^1 | p2) is non empty V128() V129() V130() set

[: the carrier of I[01], the carrier of R^1:] is set

bool [: the carrier of I[01], the carrier of R^1:] is non empty set

(#) (F,T) is complex real ext-real Element of the carrier of (Closed-Interval-TSpace (F,T))

the carrier of (Closed-Interval-TSpace (F,T)) is non empty V128() V129() V130() set

(F,T) (#) is complex real ext-real Element of the carrier of (Closed-Interval-TSpace (F,T))

L[01] (((#) (F,T)),((F,T) (#))) is V19() V22( the carrier of (Closed-Interval-TSpace (0,1))) V23( the carrier of (Closed-Interval-TSpace (F,T))) Function-like V33( the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (F,T))) Element of bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (F,T)):]

[: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (F,T)):] is non empty set

bool [: the carrier of (Closed-Interval-TSpace (0,1)), the carrier of (Closed-Interval-TSpace (F,T)):] is non empty set

c

C is V19() V22( the carrier of I[01]) V23( the carrier of R^1) Function-like V33( the carrier of I[01], the carrier of R^1) Element of bool [: the carrier of I[01], the carrier of R^1:]

C . 0 is set

C . 1 is set

[: the carrier of I[01], the carrier of (R^1 | p2):] is set

bool [: the carrier of I[01], the carrier of (R^1 | p2):] is non empty set

C is V19() V22( the carrier of I[01]) V23( the carrier of R^1) Function-like V33( the carrier of I[01], the carrier of R^1) Path of F,T

- C is V19() V22( the carrier of I[01]) V23( the carrier of R^1) Function-like V33( the carrier of I[01], the carrier of R^1) Path of T,F

(- C) . 0 is set

(- C) . 1 is set

D is V19() V22( the carrier of I[01]) V23( the carrier of R^1) Function-like V33( the carrier of I[01], the carrier of R^1) Element of bool [: the carrier of I[01], the carrier of R^1:]

D . 0 is set

D . 1 is set

T is V128() V129() V130() Element of bool the carrier of R^1

F is V128() V129() V130() Element of bool the carrier of R^1

p2 is complex real ext-real set

P is complex real ext-real set

c

C is complex real ext-real set

[.P,p2.[ is V128() V129() V130() Element of bool REAL

].c

Cl ].c

[.c

Cl F is closed V128() V129() V130() Element of bool the carrier of R^1

Cl [.P,p2.[ is V128() V129() V130() Element of bool REAL

[.P,p2.] is V128() V129() V130() closed Element of bool REAL

Cl T is closed V128() V129() V130() Element of bool the carrier of R^1

T is complex real ext-real set

P is complex real ext-real set

F is complex real ext-real set

[.T,F.] is V128() V129() V130() closed Element of bool REAL

[.P,+infty.[ is V128() V129() V130() Element of bool REAL

[.T,F.] \/ [.P,+infty.[ is V128() V129() V130() Element of bool REAL

[.T,+infty.[ is V128() V129() V130() Element of bool REAL

p2 is set

c

right_closed_halfline T is V128() V129() V130() closed Element of bool REAL

K449(T,+infty) is set

T is complex real ext-real set

P is complex real ext-real set

F is complex real ext-real set

].-infty,P.] is V128() V129() V130() Element of bool REAL

[.T,F.] is V128() V129() V130() closed Element of bool REAL

].-infty,P.] \/ [.T,F.] is V128() V129() V130() Element of bool REAL

].-infty,F.] is V128() V129() V130() Element of bool REAL

p2 is set

c

c

c

p2 is set

c

c

c

T is complex real ext-real non irrational Element of RAT

F is complex real ext-real Element of the carrier of RealSpace

T is V128() V129() V130() Element of bool the carrier of R^1

Cl T is closed V128() V129() V130() Element of bool the carrier of R^1

P is complex real ext-real set

Ball (F,P) is V128() V129() V130() Element of bool the carrier of RealSpace

c

p2 is V128() V129() V130() Element of bool the carrier of R^1

Cl p2 is closed V128() V129() V130() Element of bool the carrier of R^1

T is complex real ext-real Element of the carrier of RealSpace

F is complex real ext-real Element of the carrier of RealSpace

dist (T,F) is complex real ext-real Element of REAL

F - T is complex real ext-real set

abs (F - T) is complex real ext-real Element of REAL

T is V128() V129() V130() Element of bool the carrier of R^1

Cl T is closed V128() V129() V130() Element of bool the carrier of R^1

F is set

P is complex real ext-real Element of the carrier of RealSpace

p2 is complex real ext-real set

P + p2 is complex real ext-real set

c

C is complex real ext-real non irrational set

c

C is complex real ext-real Element of the carrier of RealSpace

C - P is complex real ext-real set

dist (P,C) is complex real ext-real Element of REAL

Ball (P,p2) is V128() V129() V130() Element of bool the carrier of RealSpace

T is V128() V129() V130() Element of bool the carrier of R^1

Cl T is closed V128() V129() V130() Element of bool the carrier of R^1

F is complex real ext-real set

P is complex real ext-real set

].F,P.[ is V128() V129() V130() open Element of bool REAL

[.F,P.] is V128() V129() V130() closed Element of bool REAL

Cl ].F,P.[ is V128() V129() V130() Element of bool REAL

REAL \ RAT is V128() V129() V130() Element of bool REAL

() is V128() V129() V130() Element of bool REAL

T is complex real ext-real set

F is complex real ext-real set

].T,F.[ is V128() V129() V130() open Element of bool REAL

RAT /\ ].T,F.[ is V128() V129() V130() V131() Element of bool REAL

() /\ ].T,F.[ is V128() V129() V130() Element of bool REAL

T is complex real ext-real set

T is complex real ext-real non irrational set

F is complex real ext-real irrational set

T + F is complex real ext-real set

the complex real ext-real integer non irrational set is complex real ext-real integer non irrational set

c

p2 is complex real ext-real integer non irrational set

p2 / c

(T + F) - T is complex real ext-real set

p2 * the complex real ext-real integer non irrational set is complex real ext-real integer non irrational set

the complex real ext-real integer non irrational set * c

(p2 * the complex real ext-real integer non irrational set ) - ( the complex real ext-real integer non irrational set * c

((p2 * the complex real ext-real integer non irrational set ) - ( the complex real ext-real integer non irrational set * c

F + T is complex real ext-real irrational set

T is complex real ext-real non irrational set

F is complex real ext-real irrational set

T + F is complex real ext-real irrational set

T is complex real ext-real irrational set

- T is complex real ext-real set

F is complex real ext-real non irrational set

- F is complex real ext-real non irrational set

T is complex real ext-real irrational set

- T is complex real ext-real irrational set

T is complex real ext-real non irrational set

F is complex real ext-real irrational set

T - F is complex real ext-real set

- F is complex real ext-real irrational set

T + (- F) is complex real ext-real irrational set

F - T is complex real ext-real set

- T is complex real ext-real non irrational set

F + (- T) is complex real ext-real irrational set

T is complex real ext-real non irrational set

F is complex real ext-real irrational set

T - F is complex real ext-real irrational set

F is complex real ext-real irrational set

T is complex real ext-real non irrational set

F - T is complex real ext-real irrational set

T is complex real ext-real non irrational set

F is complex real ext-real irrational set

T * F is complex real ext-real set

p2 is complex real ext-real integer non irrational set

P is complex real ext-real integer non irrational set

P / p2 is complex real ext-real non irrational Element of COMPLEX

C is complex real ext-real integer non irrational set

c

c

(T * F) / T is complex real ext-real Element of COMPLEX

P * C is complex real ext-real integer non irrational set

p2 * c

(P * C) / (p2 * c

T is complex real ext-real non irrational set

F is complex real ext-real irrational set

F / T is complex real ext-real Element of COMPLEX

P is complex real ext-real non irrational set

P * T is complex real ext-real non irrational set

T is complex real ext-real set

0 / 1 is empty complex real ext-real non positive non negative V36() V40() V128() V129() V130() V131() V132() V133() V134() non irrational Element of COMPLEX

T is complex real ext-real non irrational set

F is non empty complex real ext-real irrational set

T / F is complex real ext-real Element of COMPLEX

P is complex real ext-real non irrational set

P * F is complex real ext-real set

T is non empty complex real ext-real irrational set

frac T is complex real ext-real Element of REAL

[\T/] is complex real ext-real integer non irrational set

T - [\T/] is non empty complex real ext-real irrational set

T is non empty complex real ext-real irrational set

frac T is non empty complex real ext-real irrational Element of REAL

T is non empty complex real ext-real non irrational set

F is non empty complex real ext-real irrational set

T * F is complex real ext-real set

F * T is non empty complex real ext-real irrational set

T / F is complex real ext-real Element of COMPLEX

F / T is complex real ext-real Element of COMPLEX

F is complex real ext-real set

T is complex real ext-real set

P is complex real ext-real non irrational set

p2 is complex real ext-real non irrational set

frac number_e is non empty complex real ext-real irrational Element of REAL

P is complex real ext-real set

F is complex real ext-real set

p2 is complex real ext-real non irrational set

c

1 - (frac number_e) is non empty complex real ext-real irrational set

(1 - (frac number_e)) * p2 is complex real ext-real set

(frac number_e) * c

((1 - (frac number_e)) * p2) + ((frac number_e) * c

c

(frac number_e) * (c

p2 + ((frac number_e) * (c

T is V128() V129() V130() Element of bool the carrier of R^1

Cl T is closed V128() V129() V130() Element of bool the carrier of R^1

F is set

P is complex real ext-real Element of the carrier of RealSpace

p2 is complex real ext-real set

P + p2 is complex real ext-real set

c

C is non empty complex real ext-real irrational set

c

C is complex real ext-real Element of the carrier of RealSpace

C - P is complex real ext-real set

dist (P,C) is complex real ext-real Element of REAL

Ball (P,p2) is V128() V129() V130() Element of bool the carrier of RealSpace

T is V128() V129() V130() Element of bool the carrier of R^1

Cl T is closed V128() V129() V130() Element of bool the carrier of R^1

P is complex real ext-real set

F is complex real ext-real set

(F,P) is V128() V129() V130() Element of bool REAL

].F,P.[ is V128() V129() V130() open Element of bool REAL

RAT /\ ].F,P.[ is V128() V129() V130() V131() Element of bool REAL

p2 is complex real ext-real Element of the carrier of RealSpace

C is complex real ext-real set

Ball (p2,C) is V128() V129() V130() Element of bool the carrier of RealSpace

F + C is complex real ext-real set

C is complex real ext-real Element of the carrier of RealSpace

F + P is complex real ext-real set

(F + P) / 2 is complex real ext-real Element of COMPLEX

min (C,((F + P) / 2)) is complex real ext-real set

E is complex real ext-real non irrational set

(min (C,((F + P) / 2))) - F is complex real ext-real set

C - F is complex real ext-real set

F is complex real ext-real Element of the carrier of RealSpace

F - F is complex real ext-real set

dist (p2,F) is complex real ext-real Element of REAL

p2 is complex real ext-real Element of the carrier of RealSpace

C is complex real ext-real set

Ball (p2,C) is V128() V129() V130() Element of bool the carrier of RealSpace

P - C is complex real ext-real set

C is complex real ext-real Element of the carrier of RealSpace

P + F is complex real ext-real set

(P + F) / 2 is complex real ext-real Element of COMPLEX

max (C,((P + F) / 2)) is complex real ext-real set

P + C is complex real ext-real set

E is complex real ext-real non irrational set

P - (max (C,((P + F) / 2))) is complex real ext-real set

P - C is complex real ext-real set

F is complex real ext-real Element of the carrier of RealSpace

P - F is complex real ext-real set

dist (p2,F) is complex real ext-real Element of REAL

T is V128() V129() V130() Element of bool the carrier of R^1

Cl T is closed V128() V129() V130() Element of bool the carrier of R^1

P is complex real ext-real set

F is complex real ext-real set

(F,P) is V128() V129() V130() Element of bool REAL

].F,P.[ is V128() V129() V130() open Element of bool REAL

() /\ ].F,P.[ is V128() V129() V130() Element of bool REAL

p2 is complex real ext-real Element of the carrier of RealSpace

C is complex real ext-real set

Ball (p2,C) is V128() V129() V130() Element of bool the carrier of RealSpace

F + C is complex real ext-real set

C is complex real ext-real Element of the carrier of RealSpace

F + P is complex real ext-real set

(F + P) / 2 is complex real ext-real Element of COMPLEX

min (C,((F + P) / 2)) is complex real ext-real set

E is non empty complex real ext-real irrational set

(min (C,((F + P) / 2))) - F is complex real ext-real set

C - F is complex real ext-real set

F is complex real ext-real Element of the carrier of RealSpace

F - F is complex real ext-real set

dist (p2,F) is complex real ext-real Element of REAL

p2 is complex real ext-real Element of the carrier of RealSpace

C is complex real ext-real set

Ball (p2,C) is V128() V129() V130() Element of bool the carrier of RealSpace

P - C is complex real ext-real set

C is complex real ext-real Element of the carrier of RealSpace

P + F is complex real ext-real set

(P + F) / 2 is complex real ext-real Element of COMPLEX

max (C,((P + F) / 2)) is complex real ext-real set

P + C is complex real ext-real set

E is non empty complex real ext-real irrational set

P - (max (C,((P + F) / 2))) is complex real ext-real set

P - C is complex real ext-real set

F is complex real ext-real Element of the carrier of RealSpace

P - F is complex real ext-real set

dist (p2,F) is complex real ext-real Element of REAL

P is complex real ext-real set

T is complex real ext-real set

F is complex real ext-real set

(T,F) is V128() V129() V130() Element of bool REAL

].T,F.[ is V128() V129() V130() open Element of bool REAL

RAT /\ ].T,F.[ is V128() V129() V130() V131() Element of bool REAL

P is complex real ext-real set

T is complex real ext-real set

F is complex real ext-real set

(T,F) is V128() V129() V130() Element of bool REAL

].T,F.[ is V128() V129() V130() open Element of bool REAL

() /\ ].T,F.[ is V128() V129() V130() Element of bool REAL

T is V128() V129() V130() Element of bool the carrier of R^1

Cl T is closed V128() V129() V130() Element of bool the carrier of R^1

P is complex real ext-real set

F is complex real ext-real set

(F,P) is V128() V129() V130() Element of bool REAL

].F,P.[ is V128() V129() V130() open Element of bool REAL

RAT /\ ].F,P.[ is V128() V129() V130() V131() Element of bool REAL

[.F,P.] is V128() V129() V130() closed Element of bool REAL

p2 is V128() V129() V130() Element of bool the carrier of R^1

Cl p2 is closed V128() V129() V130() Element of bool the carrier of R^1

the carrier of R^1 /\ (Cl p2) is V128() V129() V130() Element of bool the carrier of R^1

C is V128() V129() V130() Element of bool the carrier of R^1

Cl C is closed V128() V129() V130() Element of bool the carrier of R^1

c

Cl c

(Cl c

C is set

C is set

D is complex real ext-real Element of the carrier of RealSpace

E is complex real ext-real set

D + E is complex real ext-real set

F is complex real ext-real Element of the carrier of RealSpace

D + P is complex real ext-real set

(D + P) / 2 is complex real ext-real Element of COMPLEX

min (F,((D + P) / 2)) is complex real ext-real set

Q is complex real ext-real non irrational set

(min (F,((D + P) / 2))) - D is complex real ext-real set

F - D is complex real ext-real set

P is complex real ext-real Element of the carrier of RealSpace

P - D is complex real ext-real set

dist (D,P) is complex real ext-real Element of REAL

Ball (D,E) is V128() V129() V130() Element of bool the carrier of RealSpace

T is V128() V129() V130() Element of bool the carrier of R^1

Cl T is closed V128() V129() V130() Element of bool the carrier of R^1

P is complex real ext-real set

F is complex real ext-real set

(F,P) is V128() V129() V130() Element of bool REAL

].F,P.[ is V128() V129() V130() open Element of bool REAL

() /\ ].F,P.[ is V128() V129() V130() Element of bool REAL

[.F,P.] is V128() V129() V130() closed Element of bool REAL

p2 is V128() V129() V130() Element of bool the carrier of R^1

Cl p2 is closed V128() V129() V130() Element of bool the carrier of R^1

the carrier of R^1 /\ (Cl p2) is V128() V129() V130() Element of bool the carrier of R^1

C is V128() V129() V130() Element of bool the carrier of R^1

Cl C is closed V128() V129() V130() Element of bool the carrier of R^1

c

Cl c

(Cl c

C is set

C is set

D is complex real ext-real Element of the carrier of RealSpace

E is complex real ext-real set

D + E is complex real ext-real set

F is complex real ext-real Element of the carrier of RealSpace

D + P is complex real ext-real set

(D + P) / 2 is complex real ext-real Element of COMPLEX

min (F,((D + P) / 2)) is complex real ext-real set

Q is non empty complex real ext-real irrational set

(min (F,((D + P) / 2))) - D is complex real ext-real set

F - D is complex real ext-real set

P is complex real ext-real Element of the carrier of RealSpace

P - D is complex real ext-real set

dist (D,P) is complex real ext-real Element of REAL

Ball (D,E) is V128() V129() V130() Element of bool the carrier of RealSpace

T is TopSpace-like connected TopStruct

the carrier of T is set

bool the carrier of T is non empty set

[#] T is non proper open closed Element of bool the carrier of T

F is open closed Element of bool the carrier of T

F ` is open closed Element of bool the carrier of T

the carrier of T \ F is set

F \/ (F `) is open closed Element of bool the carrier of T

{} T is empty V36() V40() open closed connected V128() V129() V130() V131() V132() V133() V134() Element of bool the carrier of T

T is V128() V129() V130() Element of bool the carrier of R^1

F is open closed V128() V129() V130() Element of bool the carrier of R^1

[#] R^1 is non empty non proper open closed V128() V129() V130() Element of bool the carrier of R^1

T is V128() V129() V130() Element of bool the carrier of R^1

Cl T is closed V128() V129() V130() Element of bool the carrier of R^1

F is complex real ext-real set

P is complex real ext-real set

[.F,P.[ is V128() V129() V130() Element of bool REAL

[.F,P.] is V128() V129() V130() closed Element of bool REAL

Cl [.F,P.[ is V128() V129() V130() Element of bool REAL

T is V128() V129() V130() Element of bool the carrier of R^1

Cl T is closed V128() V129() V130() Element of bool the carrier of R^1

F is complex real ext-real set

P is complex real ext-real set

].F,P.] is V128() V129() V130() Element of bool REAL

[.F,P.] is V128() V129() V130() closed Element of bool REAL

Cl ].F,P.] is V128() V129() V130() Element of bool REAL

T is V128() V129() V130() Element of bool the carrier of R^1

Cl T is closed V128() V129() V130() Element of bool the carrier of R^1

F is complex real ext-real set

P is complex real ext-real set

[.F,P.[ is V128() V129() V130() Element of bool REAL

p2 is complex real ext-real set

].P,p2.] is V128() V129() V130() Element of bool REAL

[.F,P.[ \/ ].P,p2.] is V128() V129() V130() Element of bool REAL

[.F,p2.] is V128() V129() V130() closed Element of bool REAL

c

Cl c

C is V128() V129() V130() Element of bool the carrier of R^1

Cl C is closed V128() V129() V130() Element of bool the carrier of R^1

(Cl c

[.F,P.] is V128() V129() V130() closed Element of bool REAL

[.F,P.] \/ (Cl C) is V128() V129() V130() set

[.P,p2.] is V128() V129() V130() closed Element of bool REAL

[.F,P.] \/ [.P,p2.] is V128() V129() V130() Element of bool REAL

T is V128() V129() V130() Element of bool the carrier of R^1

Cl T is closed V128() V129() V130() Element of bool the carrier of R^1

F is complex real ext-real set

{F} is non empty V36() V128() V129() V130() Element of bool REAL

T is V128() V129() V130() Element of bool REAL

F is V128() V129() V130() Element of bool the carrier of R^1

the topology of (TopSpaceMetr RealSpace) is Element of bool (bool the carrier of (TopSpaceMetr RealSpace))

the carrier of (TopSpaceMetr RealSpace) is set

bool the carrier of (TopSpaceMetr RealSpace) is non empty set

bool (bool the carrier of (TopSpaceMetr RealSpace)) is non empty set

the topology of R^1 is non empty Element of bool (bool the carrier of R^1)

bool (bool the carrier of R^1) is non empty set

T is complex real ext-real set

].-infty,T.] is V128() V129() V130() Element of bool REAL

left_closed_halfline T is V128() V129() V130() closed Element of bool REAL

K450(-infty,T) is set

T is complex real ext-real set

[.T,+infty.[ is V128() V129() V130() Element of bool REAL

right_closed_halfline T is V128() V129() V130() closed Element of bool REAL

K449(T,+infty) is set

T is V128() V129() V130() open Element of bool REAL

F is V128() V129() V130() open Element of bool REAL

T /\ F is V128() V129() V130() Element of bool REAL

p2 is V128() V129() V130() Element of bool the carrier of R^1

P is V128() V129() V130() Element of bool the carrier of R^1

P /\ p2 is V128() V129() V130() Element of bool the carrier of R^1

c

T \/ F is V128() V129() V130() Element of bool REAL

p2 is V128() V129() V130() Element of bool the carrier of R^1

P is V128() V129() V130() Element of bool the carrier of R^1

P \/ p2 is V128() V129() V130() Element of bool the carrier of R^1

c

T is ext-real set

F is ext-real set

].T,F.[ is V128() V129() V130() Element of bool REAL

c

].-infty,c

p2 is complex real ext-real set

].p2,+infty.[ is V128() V129() V130() Element of bool REAL

].-infty,c

p2 is complex real ext-real set

left_open_halfline p2 is V128() V129() V130() open Element of bool REAL

K451(-infty,p2) is set

p2 is complex real ext-real set

right_open_halfline p2 is V128() V129() V130() open Element of bool REAL

K451(p2,+infty) is set

[#] REAL is non proper V128() V129() V130() closed open Element of bool REAL

T is V128() V129() V130() Element of bool the carrier of R^1

F is ext-real set

P is ext-real set

].F,P.[ is V128() V129() V130() Element of bool REAL

T is V128() V129() V130() Element of bool the carrier of R^1

F is complex real ext-real set

].-infty,F.] is V128() V129() V130() Element of bool REAL

T is V128() V129() V130() Element of bool the carrier of R^1

F is complex real ext-real set

[.F,+infty.[ is V128() V129() V130() Element of bool REAL

T is complex real ext-real set

[.T,+infty.[ is V128() V129() V130() Element of bool REAL

{T} is non empty V36() V128() V129() V130() Element of bool REAL

].T,+infty.[ is V128() V129() V130() Element of bool REAL

{T} \/ ].T,+infty.[ is non empty V128() V129() V130() Element of bool REAL

F is set

P is complex real ext-real set

F is set

P is complex real ext-real set

T is complex real ext-real set

].-infty,T.] is V128() V129() V130() Element of bool REAL

{T} is non empty V36() V128() V129() V130() Element of bool REAL

].-infty,T.[ is V128() V129() V130() Element of bool REAL

{T} \/ ].-infty,T.[ is non empty V128() V129() V130() Element of bool REAL

F is set

P is complex real ext-real set

F is set

P is complex real ext-real set

T is complex real ext-real set

].T,+infty.[ is V128() V129() V130() Element of bool REAL

T + 1 is complex real ext-real set

].-infty,T.] is V128() V129() V130() Element of bool REAL

].-infty,T.[ is V128() V129() V130() Element of bool REAL

T - 1 is complex real ext-real set

[.T,+infty.[ is V128() V129() V130() Element of bool REAL

T is complex real ext-real set

].T,+infty.[ is non empty V128() V129() V130() Element of bool REAL

T is complex real ext-real set

[.T,+infty.[ is non empty V128() V129() V130() Element of bool REAL

T - 1 is complex real ext-real set

T is complex real ext-real set

].-infty,T.] is non empty V128() V129() V130() Element of bool REAL

T + 1 is complex real ext-real set

T is complex real ext-real set

].-infty,T.[ is non empty V128() V129() V130() Element of bool REAL

T + 1 is complex real ext-real set

T is V128() V129() V130() Element of bool the carrier of R^1

Cl T is closed V128() V129() V130() Element of bool the carrier of R^1

F is complex real ext-real set

].F,+infty.[ is non empty V128() V129() V130() Element of bool REAL

[.F,+infty.[ is non empty V128() V129() V130() Element of bool REAL

P is V128() V129() V130() Element of bool the carrier of R^1

p2 is V128() V129() V130() Element of bool the carrier of R^1

Cl P is closed V128() V129() V130() Element of bool the carrier of R^1

{F} is non empty V36() V128() V129() V130() Element of bool REAL

P \/ {F} is non empty V128() V129() V130() set

T is complex real ext-real set

].T,+infty.[ is non empty V128() V129() V130() Element of bool REAL

Cl ].T,+infty.[ is non empty V128() V129() V130() Element of bool REAL

[.T,+infty.[ is non empty V128() V129() V130() Element of bool REAL

F is V128() V129() V130() Element of bool the carrier of R^1

Cl F is closed V128() V129() V130() Element of bool the carrier of R^1

T is V128() V129() V130() Element of bool the carrier of R^1

Cl T is closed V128() V129() V130() Element of bool the carrier of R^1

F is complex real ext-real set

].-infty,F.[ is non empty V128() V129() V130() Element of bool REAL

].-infty,F.] is non empty V128() V129() V130() Element of bool REAL

P is V128() V129() V130() Element of bool the carrier of R^1

p2 is V128() V129() V130() Element of bool the carrier of R^1

Cl P is closed V128() V129() V130() Element of bool the carrier of R^1

{F} is non empty V36() V128() V129() V130() Element of bool REAL

P \/ {F} is non empty V128() V129() V130() set

T is complex real ext-real set

].-infty,T.[ is non empty V128() V129() V130() Element of bool REAL

Cl ].-infty,T.[ is non empty V128() V129() V130() Element of bool REAL

].-infty,T.] is non empty V128() V129() V130() Element of bool REAL

F is V128() V129() V130() Element of bool the carrier of R^1

Cl F is closed V128() V129() V130() Element of bool the carrier of R^1

T is V128() V129() V130() Element of bool the carrier of R^1

F is V128() V129() V130() Element of bool the carrier of R^1

P is complex real ext-real set

].-infty,P.[ is non empty V128() V129() V130() Element of bool REAL

].P,+infty.[ is non empty V128() V129() V130() Element of bool REAL

Cl F is closed V128() V129() V130() Element of bool the carrier of R^1

[.P,+infty.[ is non empty V128() V129() V130() Element of bool REAL

Cl T is closed V128() V129() V130() Element of bool the carrier of R^1

].-infty,P.] is non empty V128() V129() V130() Element of bool REAL

T is V128() V129() V130() Element of bool the carrier of R^1

Cl T is closed V128() V129() V130() Element of bool the carrier of R^1

P is complex real ext-real set

F is complex real ext-real set

[.F,P.[ is V128() V129() V130() Element of bool REAL

].P,+infty.[ is non empty V128() V129() V130() Element of bool REAL

[.F,P.[ \/ ].P,+infty.[ is non empty V128() V129() V130() Element of bool REAL

[.F,+infty.[ is non empty V128() V129() V130() Element of bool REAL

p2 is V128() V129() V130() Element of bool the carrier of R^1

Cl p2 is closed V128() V129() V130() Element of bool the carrier of R^1

c

Cl c

(Cl p2) \/ (Cl c

[.P,+infty.[ is non empty V128() V129() V130() Element of bool REAL

[.F,P.] is V128() V129() V130() closed Element of bool REAL

T is V128() V129() V130() Element of bool the carrier of R^1

Cl T is closed V128() V129() V130() Element of bool the carrier of R^1

P is complex real ext-real set

F is complex real ext-real set

].F,P.[ is V128() V129() V130() open Element of bool REAL

].P,+infty.[ is non empty V128() V129() V130() Element of bool REAL

].F,P.[ \/ ].P,+infty.[ is non empty V128() V129() V130() Element of bool REAL

[.F,+infty.[ is non empty V128() V129() V130() Element of bool REAL

p2 is V128() V129() V130() Element of bool the carrier of R^1

Cl p2 is closed V128() V129() V130() Element of bool the carrier of R^1

c

Cl c

(Cl p2) \/ (Cl c

[.P,+infty.[ is non empty V128() V129() V130() Element of bool REAL

[.F,P.] is V128() V129() V130() closed Element of bool REAL

T is V128() V129() V130() Element of bool the carrier of R^1

Cl T is closed V128() V129() V130() Element of bool the carrier of R^1

P is complex real ext-real set

F is complex real ext-real set

p2 is complex real ext-real set

(F,P) is V128() V129() V130() Element of bool REAL

].F,P.[ is V128() V129() V130() open Element of bool REAL

RAT /\ ].F,P.[ is V128() V129() V130() V131() Element of bool REAL

].P,p2.[ is V128() V129() V130() open Element of bool REAL

(F,P) \/ ].P,p2.[ is V128() V129() V130() Element of bool REAL

].p2,+infty.[ is non empty V128() V129() V130() Element of bool REAL

((F,P) \/ ].P,p2.[) \/ ].p2,+infty.[ is non empty V128() V129() V130() Element of bool REAL

[.F,+infty.[ is non empty V128() V129() V130() Element of bool REAL

].P,p2.[ \/ ].p2,+infty.[ is non empty V128() V129() V130() Element of bool REAL

C is V128() V129() V130() Element of bool the carrier of R^1

(F,P) \/ C is V128() V129() V130() set

c

Cl c

Cl C is closed V128() V129() V130() Element of bool the carrier of R^1

(Cl c

[.P,+infty.[ is non empty V128() V129() V130() Element of bool REAL

(Cl c

[.F,P.] is V128() V129() V130() closed Element of bool REAL

[.F,P.] \/ [.P,+infty.[ is non empty V128() V129() V130() Element of bool REAL

T is complex real ext-real set

F is complex real ext-real set

(T,F) is V128() V129() V130() Element of bool REAL

].T,F.[ is V128() V129() V130() open Element of bool REAL

() /\ ].T,F.[ is V128() V129() V130() Element of bool REAL

(T,F) is V128() V129() V130() Element of bool REAL

RAT /\ ].T,F.[ is V128() V129() V130() V131() Element of bool REAL

P is set

T is complex real ext-real set

F is complex real ext-real set

(T,F) is V128() V129() V130() Element of bool REAL

].T,F.[ is V128() V129() V130() open Element of bool REAL

RAT /\ ].T,F.[ is V128() V129() V130() V131() Element of bool REAL

REAL \ (T,F) is V128() V129() V130() Element of bool REAL

].-infty,T.] is non empty V128() V129() V130() Element of bool REAL

(T,F) is V128() V129() V130() Element of bool REAL

() /\ ].T,F.[ is V128() V129() V130() Element of bool REAL

].-infty,T.] \/ (T,F) is non empty V128() V129() V130() Element of bool REAL

[.F,+infty.[ is non empty V128() V129() V130() Element of bool REAL

(].-infty,T.] \/ (T,F)) \/ [.F,+infty.[ is non empty V128() V129() V130() Element of bool REAL

P is set

p2 is complex real ext-real set

p2 is complex real ext-real set

p2 is complex real ext-real set

p2 is complex real ext-real set

p2 is complex real ext-real set

P is set

p2 is complex real ext-real set

F is complex real ext-real set

T is complex real ext-real set

[.T,+infty.[ is non empty V128() V129() V130() Element of bool REAL

].T,F.[ is V128() V129() V130() open Element of bool REAL

].F,+infty.[ is non empty V128() V129() V130() Element of bool REAL

].T,F.[ \/ ].F,+infty.[ is non empty V128() V129() V130() Element of bool REAL

[.T,+infty.[ \ (].T,F.[ \/ ].F,+infty.[) is V128() V129() V130() Element of bool REAL

{T} is non empty V36() V128() V129() V130() Element of bool REAL

{F} is non empty V36() V128() V129() V130() Element of bool REAL

{T} \/ {F} is non empty V36() V128() V129() V130() Element of bool REAL

[.T,F.] is V128() V129() V130() closed Element of bool REAL

[.F,+infty.[ is non empty V128() V129() V130() Element of bool REAL

[.T,F.] \/ [.F,+infty.[ is non empty V128() V129() V130() Element of bool REAL

{T,F} is non empty V36() V128() V129() V130() set

{T,F} \/ ].T,F.[ is non empty V128() V129() V130() set

({T,F} \/ ].T,F.[) \/ [.F,+infty.[ is non empty V128() V129() V130() set

{F} \/ ].F,+infty.[ is non empty V128() V129() V130() Element of bool REAL

({T,F} \/ ].T,F.[) \/ ({F} \/ ].F,+infty.[) is non empty V128() V129() V130() set

({T,F} \/ ].T,F.[) \/ {F} is non empty V128() V129() V130() set

(({T,F} \/ ].T,F.[) \/ {F}) \/ ].F,+infty.[ is non empty V128() V129() V130() set

{T,F} \/ {F} is non empty V36() V128() V129() V130() set

({T,F} \/ {F}) \/ ].T,F.[ is non empty V128() V129() V130() set

(({T,F} \/ {F}) \/ ].T,F.[) \/ ].F,+infty.[ is non empty V128() V129() V130() set

({T,F} \/ ].T,F.[) \/ ].F,+infty.[ is non empty V128() V129() V130() set

{T,F} \/ (].T,F.[ \/ ].F,+infty.[) is non empty V128() V129() V130() set

4 is non empty natural complex real ext-real positive non negative V128() V129() V130() V131() V132() V133() integer non irrational Element of NAT

(2,4) is V128() V129() V130() Element of bool REAL

].2,4.[ is V128() V129() V130() open Element of bool REAL

RAT /\ ].2,4.[ is V128() V129() V130() V131() Element of bool REAL

].4,5.[ is V128() V129() V130() open Element of bool REAL

(2,4) \/ ].4,5.[ is V128() V129() V130() Element of bool REAL

].5,+infty.[ is non empty V128() V129() V130() Element of bool REAL

((2,4) \/ ].4,5.[) \/ ].5,+infty.[ is non empty V128() V129() V130() Element of bool REAL

].-infty,2.] is non empty V128() V129() V130() Element of bool REAL

(2,4) is V128() V129() V130() Element of bool REAL

() /\ ].2,4.[ is V128() V129() V130() Element of bool REAL

].-infty,2.] \/ (2,4) is non empty V128() V129() V130() Element of bool REAL

{4} is non empty V36() V128() V129() V130() V131() V132() V133() Element of bool REAL

(].-infty,2.] \/ (2,4)) \/ {4} is non empty V128() V129() V130() Element of bool REAL

{5} is non empty V36() V128() V129() V130() V131() V132() V133() Element of bool REAL

((].-infty,2.] \/ (2,4)) \/ {4}) \/ {5} is non empty V128() V129() V130() Element of bool REAL

].-infty,4.] is non empty V128() V129() V130() Element of bool REAL

T is set

F is complex real ext-real set

F is complex real ext-real set

F is complex real ext-real set

T is V128() V129() V130() Element of bool the carrier of R^1

T ` is V128() V129() V130() Element of bool the carrier of R^1

the carrier of R^1 \ T is V128() V129() V130() set

].4,5.[ \/ ].5,+infty.[ is non empty V128() V129() V130() Element of bool REAL

].4,+infty.[ is non empty V128() V129() V130() Element of bool REAL

F is set

P is complex real ext-real set

P is complex real ext-real set

P is complex real ext-real set

(2,4) \/ (].4,5.[ \/ ].5,+infty.[) is non empty V128() V129() V130() Element of bool REAL

REAL \ ((2,4) \/ (].4,5.[ \/ ].5,+infty.[)) is V128() V129() V130() Element of bool REAL

REAL \ (2,4) is V128() V129() V130() Element of bool REAL

(REAL \ (2,4)) \ (].4,5.[ \/ ].5,+infty.[) is V128() V129() V130() Element of bool REAL

[.4,+infty.[ is non empty V128() V129() V130() Element of bool REAL

(].-infty,2.] \/ (2,4)) \/ [.4,+infty.[ is non empty V128() V129() V130() Element of bool REAL

((].-infty,2.] \/ (2,4)) \/ [.4,+infty.[) \ (].4,5.[ \/ ].5,+infty.[) is V128() V129() V130() Element of bool REAL

[.4,+infty.[ \ (].4,5.[ \/ ].5,+infty.[) is V128() V129() V130() Element of bool REAL

([.4,+infty.[ \ (].4,5.[ \/ ].5,+infty.[)) \/ (].-infty,2.] \/ (2,4)) is non empty V128() V129() V130() Element of bool REAL

{4} \/ {5} is non empty V36() V128() V129() V130() V131() V132() V133() Element of bool REAL

(].-infty,2.] \/ (2,4)) \/ ({4} \/ {5}) is non empty V128() V129() V130() Element of bool REAL

T is V128() V129() V130() Element of bool the carrier of R^1

F is complex real ext-real set

{F} is non empty V36() V128() V129() V130() Element of bool REAL

T ` is V128() V129() V130() Element of bool the carrier of R^1

the carrier of R^1 \ T is V128() V129() V130() set

].-infty,F.[ is non empty V128() V129() V130() Element of bool REAL

].F,+infty.[ is non empty V128() V129() V130() Element of bool REAL

].-infty,F.[ \/ ].F,+infty.[ is non empty V128() V129() V130() Element of bool REAL

(2,4) \/ {4} is non empty V128() V129() V130() Element of bool REAL

((2,4) \/ {4}) \/ {5} is non empty V128() V129() V130() Element of bool REAL

].1,+infty.[ is non empty V128() V129() V130() Element of bool REAL

T is set

F is complex real ext-real set

[.1,+infty.[ is non empty V128() V129() V130() Element of bool REAL

].-infty,1.[ is non empty V128() V129() V130() Element of bool REAL

].-infty,1.[ /\ (((].-infty,2.] \/ (2,4)) \/ {4}) \/ {5}) is V128() V129() V130() Element of bool REAL

T is set

F is complex real ext-real set

].-infty,2.] \/ (((2,4) \/ {4}) \/ {5}) is non empty V128() V129() V130() Element of bool REAL

].-infty,1.[ /\ (].-infty,2.] \/ (((2,4) \/ {4}) \/ {5})) is V128() V129() V130() Element of bool REAL

].-infty,1.[ /\ ].-infty,2.] is V128() V129() V130() Element of bool REAL

].1,+infty.[ /\ (((].-infty,2.] \/ (2,4)) \/ {4}) \/ {5}) is V128() V129() V130() Element of bool REAL

].1,2.] is V128() V129() V130() Element of bool REAL

].1,2.] \/ (2,4) is V128() V129() V130() Element of bool REAL

(].1,2.] \/ (2,4)) \/ {4} is non empty V128() V129() V130() Element of bool REAL

((].1,2.] \/ (2,4)) \/ {4}) \/ {5} is non empty V128() V129() V130() Element of bool REAL

].-infty,2.] \/ (((2,4) \/ {4}) \/ {5}) is non empty V128() V129() V130() Element of bool REAL

].1,+infty.[ /\ (].-infty,2.] \/ (((2,4) \/ {4}) \/ {5})) is V128() V129() V130() Element of bool REAL

].1,+infty.[ /\ ].-infty,2.] is V128() V129() V130() Element of bool REAL

].1,+infty.[ /\ (((2,4) \/ {4}) \/ {5}) is V128() V129() V130() Element of bool REAL

(].1,+infty.[ /\ ].-infty,2.]) \/ (].1,+infty.[ /\ (((2,4) \/ {4}) \/ {5})) is V128() V129() V130() Element of bool REAL

(].1,+infty.[ /\ ].-infty,2.]) \/ (((2,4) \/ {4}) \/ {5}) is non empty V128() V129() V130() Element of bool REAL

].1,2.] \/ (((2,4) \/ {4}) \/ {5}) is non empty V128() V129() V130() Element of bool REAL

].-infty,1.[ \/ ].1,+infty.[ is non empty V128() V129() V130() Element of bool REAL

(].-infty,1.[ \/ ].1,+infty.[) /\ (((].-infty,2.] \/ (2,4)) \/ {4}) \/ {5}) is V128() V129() V130() Element of bool REAL

].-infty,1.[ \/ ].1,2.] is non empty V128() V129() V130() Element of bool REAL

(].-infty,1.[ \/ ].1,2.]) \/ (2,4) is non empty V128() V129() V130() Element of bool REAL

((].-infty,1.[ \/ ].1,2.]) \/ (2,4)) \/ {4} is non empty V128() V129() V130() Element of bool REAL

(((].-infty,1.[ \/ ].1,2.]) \/ (2,4)) \/ {4}) \/ {5} is non empty V128() V129() V130() Element of bool REAL

].-infty,1.[ \/ (].1,+infty.[ /\ (((].-infty,2.] \/ (2,4)) \/ {4}) \/ {5})) is non empty V128() V129() V130() Element of bool REAL

{4} \/ {5} is non empty V36() V128() V129() V130() V131() V132() V133() Element of bool REAL

(].1,2.] \/ (2,4)) \/ ({4} \/ {5}) is non empty V128() V129() V130() Element of bool REAL

].-infty,1.[ \/ ((].1,2.] \/ (2,4)) \/ ({4} \/ {5})) is non empty V128() V129() V130() Element of bool REAL

((].-infty,1.[ \/ ].1,2.]) \/ (2,4)) \/ ({4} \/ {5}) is non empty V128() V129() V130() Element of bool REAL

T is V128() V129() V130() Element of bool the carrier of R^1

T ` is V128() V129() V130() Element of bool the carrier of R^1

the carrier of R^1 \ T is V128() V129() V130() set

F is complex real ext-real set

P is complex real ext-real set

{F} is non empty V36() V128() V129() V130() Element of bool REAL

[.P,+infty.[ is non empty V128() V129() V130() Element of bool REAL

{F} \/ [.P,+infty.[ is non empty V128() V129() V130() Element of bool REAL

].-infty,F.[ is non empty V128() V129() V130() Element of bool REAL

].F,P.[ is V128() V129() V130() open Element of bool REAL

].-infty,F.[ \/ ].F,P.[ is non empty V128() V129() V130() Element of bool REAL

REAL \ [.P,+infty.[ is V128() V129() V130() Element of bool REAL

(REAL \ [.P,+infty.[) \ {F} is V128() V129() V130() Element of bool REAL

].-infty,P.[ is non empty V128() V129() V130() Element of bool REAL

].-infty,P.[ \ {F} is V128() V129() V130() Element of bool REAL

T is V128() V129() V130() Element of bool the carrier of R^1

Cl T is closed V128() V129() V130() Element of bool the carrier of R^1

P is complex real ext-real set

F is complex real ext-real set

].-infty,F.[ is non empty V128() V129() V130() Element of bool REAL

].F,P.[ is V128() V129() V130() open Element of bool REAL

].-infty,F.[ \/ ].F,P.[ is non empty V128() V129() V130() Element of bool REAL

].-infty,P.] is non empty V128() V129() V130() Element of bool REAL

c

Cl c

[.F,P.] is V128() V129() V130() closed Element of bool REAL

p2 is V128() V129() V130() Element of bool the carrier of R^1

Cl p2 is closed V128() V129() V130() Element of bool the carrier of R^1

(Cl p2) \/ (Cl c

].-infty,F.] is non empty V128() V129() V130() Element of bool REAL

].-infty,F.] \/ [.F,P.] is non empty V128() V129() V130() Element of bool REAL

T is V128() V129() V130() Element of bool the carrier of R^1

Cl T is closed V128() V129() V130() Element of bool the carrier of R^1

P is complex real ext-real set

F is complex real ext-real set

].-infty,F.[ is non empty V128() V129() V130() Element of bool REAL

].F,P.] is V128() V129() V130() Element of bool REAL

].-infty,F.[ \/ ].F,P.] is non empty V128() V129() V130() Element of bool REAL

].-infty,P.] is non empty V128() V129() V130() Element of bool REAL

c

Cl c

[.F,P.] is V128() V129() V130() closed Element of bool REAL

p2 is V128() V129() V130() Element of bool the carrier of R^1

Cl p2 is closed V128() V129() V130() Element of bool the carrier of R^1

(Cl p2) \/ (Cl c

].-infty,F.] is non empty V128() V129() V130() Element of bool REAL

].-infty,F.] \/ [.F,P.] is non empty V128() V129() V130() Element of bool REAL

T is V128() V129() V130() Element of bool the carrier of R^1

Cl T is closed V128() V129() V130() Element of bool the carrier of R^1

P is complex real ext-real set

F is complex real ext-real set

p2 is complex real ext-real set

].-infty,F.[ is non empty V128() V129() V130() Element of bool REAL

].F,P.] is V128() V129() V130() Element of bool REAL

].-infty,F.[ \/ ].F,P.] is non empty V128() V129() V130() Element of bool REAL

(P,p2) is V128() V129() V130() Element of bool REAL

].P,p2.[ is V128() V129() V130() open Element of bool REAL

() /\ ].P,p2.[ is V128() V129() V130() Element of bool REAL

(].-infty,F.[ \/ ].F,P.]) \/ (P,p2) is non empty V128() V129() V130() Element of bool REAL

{p2} is non empty V36() V128() V129() V130() Element of bool REAL

((].-infty,F.[ \/ ].F,P.]) \/ (P,p2)) \/ {p2} is non empty V128() V129() V130() Element of bool REAL

].-infty,p2.] is non empty V128() V129() V130() Element of bool REAL

c

C is V128() V129() V130() Element of bool the carrier of R^1

c

C is V128() V129() V130() Element of bool the carrier of R^1

(c

Cl ((c

D is V128() V129() V130() Element of bool the carrier of R^1

Cl D is closed V128() V129() V130() Element of bool the carrier of R^1

(Cl ((c

(Cl ((c

Cl (c

Cl C is closed V128() V129() V130() Element of bool the carrier of R^1

(Cl (c

((Cl (c

].-infty,P.] is non empty V128() V129() V130() Element of bool REAL

].-infty,P.] \/ (Cl C) is non empty V128() V129() V130() set

(].-infty,P.] \/ (Cl C)) \/ D is non empty V128() V129() V130() set

[.P,p2.] is V128() V129() V130() closed Element of bool REAL

].-infty,P.] \/ [.P,p2.] is non empty V128() V129() V130() Element of bool REAL

(].-infty,P.] \/ [.P,p2.]) \/ D is non empty V128() V129() V130() set

].-infty,p2.] \/ D is non empty V128() V129() V130() set

T is V128() V129() V130() Element of bool the carrier of R^1

Cl T is closed V128() V129() V130() Element of bool the carrier of R^1

P is complex real ext-real set

F is complex real ext-real set

p2 is complex real ext-real set

].-infty,F.[ is non empty V128() V129() V130() Element of bool REAL

].F,P.] is V128()