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
c5 is set
C is set
{T,F,P,p2,c5,C} is non empty V36() set
{T,P,C} is non empty V36() set
{F,p2,c5} is non empty V36() set
{T,P,C} \/ {F,p2,c5} is non empty V36() set
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
c5 is set
C is set
{T,F,P,p2,c5,C} is non empty V36() set
card {T,F,P,p2,c5,C} is natural complex real ext-real V128() V129() V130() V131() V132() V133() integer non irrational Element of omega
{T,F,P,p2,c5} is non empty V36() set
{C} is non empty V36() set
{T,F,P,p2,c5} \/ {C} is non empty V36() set
card {T,F,P,p2,c5} is natural complex real ext-real V128() V129() V130() V131() V132() V133() integer non irrational Element of omega
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
c5 is set
C is set
C is set
{T,F,P,p2,c5,C,C} is non empty V36() set
card {T,F,P,p2,c5,C,C} is natural complex real ext-real V128() V129() V130() V131() V132() V133() integer non irrational Element of omega
{T,F,P,p2,c5,C} is non empty V36() set
{C} is non empty V36() set
{T,F,P,p2,c5,C} \/ {C} is non empty V36() set
card {T,F,P,p2,c5,C} is natural complex real ext-real V128() V129() V130() V131() V132() V133() integer non irrational Element of omega
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
c5 is set
C is set
{p2,c5,C} is non empty V36() set
T is set
F is set
P is set
{T,F,P} is non empty V36() set
p2 is set
c5 is set
C is set
{p2,c5,C} is non empty V36() set
T is set
F is set
P is set
p2 is set
c5 is set
C is set
{T,F,P,p2,c5,C} is non empty V36() set
C is set
{C} is non empty V36() set
T is set
F is set
P is set
p2 is set
c5 is set
C is set
C is set
T is set
F is set
P is set
p2 is set
c5 is set
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
c5 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 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
c5 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 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
c5 is complex real ext-real set
C is complex real ext-real set
[.P,p2.[ is V128() V129() V130() Element of bool REAL
].c5,C.] is V128() V129() V130() Element of bool REAL
Cl ].c5,C.] is V128() V129() V130() Element of bool REAL
[.c5,C.] is V128() V129() V130() closed Element of bool REAL
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
c5 is complex real ext-real Element of REAL
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
c5 is complex real ext-real set
c5 is complex real ext-real set
c5 is complex real ext-real set
p2 is set
c5 is complex real ext-real set
c5 is complex real ext-real set
c5 is complex real ext-real set
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
c5 is complex real ext-real Element of the carrier of RealSpace
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
c5 is complex real ext-real Element of the carrier of RealSpace
C is complex real ext-real non irrational set
c5 - P is complex real ext-real set
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
c5 is complex real ext-real integer non irrational set
p2 is complex real ext-real integer non irrational set
p2 / c5 is complex real ext-real non irrational Element of COMPLEX
(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 * c5 is complex real ext-real integer non irrational set
(p2 * the complex real ext-real integer non irrational set ) - ( the complex real ext-real integer non irrational set * c5) is complex real ext-real integer non irrational set
((p2 * the complex real ext-real integer non irrational set ) - ( the complex real ext-real integer non irrational set * c5)) / ( the complex real ext-real integer non irrational set * c5) is complex real ext-real non irrational Element of COMPLEX
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
c5 is complex real ext-real integer non irrational set
c5 / C is complex real ext-real non irrational Element of COMPLEX
(T * F) / T is complex real ext-real Element of COMPLEX
P * C is complex real ext-real integer non irrational set
p2 * c5 is complex real ext-real integer non irrational set
(P * C) / (p2 * c5) is complex real ext-real non irrational Element of COMPLEX
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
c5 is complex real ext-real non irrational set
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) * c5 is complex real ext-real set
((1 - (frac number_e)) * p2) + ((frac number_e) * c5) is complex real ext-real set
c5 - p2 is complex real ext-real non irrational set
(frac number_e) * (c5 - p2) is complex real ext-real set
p2 + ((frac number_e) * (c5 - p2)) 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 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
c5 is complex real ext-real Element of the carrier of RealSpace
C is non empty complex real ext-real irrational set
c5 - P is complex real ext-real set
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
c5 is V128() V129() V130() Element of bool the carrier of R^1
Cl c5 is closed V128() V129() V130() Element of bool the carrier of R^1
(Cl c5) /\ (Cl p2) is closed V128() V129() V130() Element of bool the carrier of R^1
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
c5 is V128() V129() V130() Element of bool the carrier of R^1
Cl c5 is closed V128() V129() V130() Element of bool the carrier of R^1
(Cl c5) /\ (Cl p2) is closed V128() V129() V130() Element of bool the carrier of R^1
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
c5 is V128() V129() V130() Element of bool the carrier of R^1
Cl c5 is closed 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
(Cl c5) \/ (Cl C) is closed V128() V129() V130() Element of bool the carrier of R^1
[.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
c5 is V128() V129() V130() 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
c5 is V128() V129() V130() Element of bool REAL
T is ext-real set
F is ext-real set
].T,F.[ is V128() V129() V130() Element of bool REAL
c5 is complex real ext-real set
].-infty,c5.[ is V128() V129() V130() Element of bool REAL
p2 is complex real ext-real set
].p2,+infty.[ is V128() V129() V130() Element of bool REAL
].-infty,c5.[ /\ ].p2,+infty.[ is V128() V129() V130() Element of bool REAL
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
c5 is V128() V129() V130() Element of bool the carrier of R^1
Cl c5 is closed V128() V129() V130() Element of bool the carrier of R^1
(Cl p2) \/ (Cl c5) 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
[.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
c5 is V128() V129() V130() Element of bool the carrier of R^1
Cl c5 is closed V128() V129() V130() Element of bool the carrier of R^1
(Cl p2) \/ (Cl c5) 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
[.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
c5 is V128() V129() V130() Element of bool the carrier of R^1
Cl c5 is closed 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 c5) \/ (Cl C) 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 c5) \/ [.P,+infty.[ is non empty V128() V129() V130() set
[.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
c5 is V128() V129() V130() Element of bool the carrier of R^1
Cl c5 is closed V128() V129() V130() Element of bool the carrier of R^1
[.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 c5) is closed V128() V129() V130() Element of bool the carrier of R^1
].-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
c5 is V128() V129() V130() Element of bool the carrier of R^1
Cl c5 is closed V128() V129() V130() Element of bool the carrier of R^1
[.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 c5) is closed V128() V129() V130() Element of bool the carrier of R^1
].-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
c5 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
c5 \/ C 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
(c5 \/ C) \/ C is V128() V129() V130() Element of bool the carrier of R^1
Cl ((c5 \/ C) \/ C) is closed V128() V129() V130() Element of bool the carrier of R^1
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 ((c5 \/ C) \/ C)) \/ (Cl D) is closed V128() V129() V130() Element of bool the carrier of R^1
(Cl ((c5 \/ C) \/ C)) \/ D is V128() V129() V130() Element of bool the carrier of R^1
Cl (c5 \/ C) is closed 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 (c5 \/ C)) \/ (Cl C) is closed V128() V129() V130() Element of bool the carrier of R^1
((Cl (c5 \/ C)) \/ (Cl C)) \/ D is V128() V129() V130() Element of bool the carrier of R^1
].-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() 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
c5 is complex real ext-real set
{c5} is non empty V36() V128() V129() V130() Element of bool REAL
(((].-infty,F.[ \/ ].F,P.]) \/ (P,p2)) \/ {p2}) \/ {c5} is non empty V128() V129() V130() Element of bool REAL
].-infty,p2.] is non empty V128() V129() V130() Element of bool REAL
].-infty,p2.] \/ {c5} is non empty V128() V129() V130() Element of bool REAL
C 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
C \/ C is V128() V129() V130() Element of bool the carrier of R^1
D is V128() V129() V130() Element of bool the carrier of R^1
(C \/ C) \/ D is V128() V129() V130() Element of bool the carrier of R^1
E is V128() V129() V130() Element of bool the carrier of R^1
((C \/ C) \/ D) \/ E is V128() V129() V130() Element of bool the carrier of R^1
Cl (((C \/ C) \/ D) \/ E) is closed V128() V129() V130() Element of bool the carrier of R^1
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
(Cl (((C \/ C) \/ D) \/ E)) \/ (Cl F) is closed V128() V129() V130() Element of bool the carrier of R^1
(Cl (((C \/ C) \/ D) \/ E)) \/ {c5} is non empty V128() V129() V130() 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
F is complex real ext-real set
P is complex real ext-real set
].-infty,F.] is non empty V128() V129() V130() Element of bool REAL
{P} is non empty V36() V128() V129() V130() Element of bool REAL
].-infty,F.] \/ {P} is non empty V128() V129() V130() Element of bool REAL
].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
REAL \ ].-infty,F.] is V128() V129() V130() Element of bool REAL
(REAL \ ].-infty,F.]) \ {P} is V128() V129() V130() Element of bool REAL
].F,+infty.[ is non empty V128() V129() V130() Element of bool REAL
].F,+infty.[ \ {P} 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
F is complex real ext-real set
{F} is non empty V36() V128() V129() V130() Element of bool REAL
[.T,+infty.[ \/ {F} is non empty V128() V129() V130() Element of bool REAL
min (T,F) is complex real ext-real set
(min (T,F)) - 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
F is complex real ext-real set
{F} is non empty V36() V128() V129() V130() Element of bool REAL
].-infty,T.] \/ {F} is non empty V128() V129() V130() Element of bool REAL
max (T,F) is complex real ext-real set
(max (T,F)) + 1 is complex real ext-real set
T is TopStruct
the carrier of T is set
bool the carrier of T is non empty set
F is Element of bool the carrier of T
P is Element of bool the carrier of T
F ` is Element of bool the carrier of T
the carrier of T \ F is set
P ` is Element of bool the carrier of T
the carrier of T \ P is set
(P `) ` is Element of bool the carrier of T
the carrier of T \ (P `) is set
{} R^1 is empty proper V36() V40() open closed connected V128() V129() V130() V131() V132() V133() V134() Element of bool the carrier of R^1
F 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
the carrier of R^1 \ F is V128() V129() V130() 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
(F `) ` is V128() V129() V130() Element of bool the carrier of R^1
the carrier of R^1 \ (F `) is V128() V129() V130() set
T is compact V128() V129() V130() Element of bool the carrier of R^1
F is V128() V129() V130() Element of bool REAL
T is compact V128() V129() V130() Element of bool the carrier of R^1
F is V128() V129() V130() Element of bool REAL
lower_bound F is complex real ext-real Element of REAL
upper_bound F is complex real ext-real Element of REAL
P is complex real ext-real set
T is non empty connected compact V128() V129() V130() Element of bool the carrier of R^1
F is V128() V129() V130() Element of bool REAL
lower_bound F is complex real ext-real Element of REAL
upper_bound F is complex real ext-real Element of REAL
[.(lower_bound F),(upper_bound F).] is V128() V129() V130() closed Element of bool REAL
P is set
p2 is complex real ext-real set
T is connected 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
p2 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
{P} is non empty V36() V128() V129() V130() Element of bool REAL
REAL \ {P} is V128() V129() V130() Element of bool REAL
].-infty,P.[ \/ ].P,+infty.[ is non empty V128() V129() V130() Element of bool REAL
c5 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
c5 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
T is connected 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() closed Element of bool REAL
p2 is set
{ b1 where b1 is complex real ext-real Element of REAL : ( F <= b1 & b1 <= P ) } is set
c5 is complex real ext-real Element of REAL
T is non empty connected compact V128() V129() V130() Element of bool the carrier of R^1
F is non empty V128() V129() V130() Element of bool REAL
upper_bound F is complex real ext-real Element of REAL
lower_bound F is complex real ext-real Element of REAL
[.(lower_bound F),(upper_bound F).] is V128() V129() V130() closed Element of bool REAL
T is non empty connected compact V128() V129() V130() Element of bool the carrier of R^1
F is non empty V128() V129() V130() closed_interval interval Element of bool REAL
lower_bound F is complex real ext-real Element of REAL
upper_bound F is complex real ext-real Element of REAL
[.(lower_bound F),(upper_bound F).] is V128() V129() V130() closed Element of bool REAL
P is complex real ext-real Element of the carrier of R^1
p2 is complex real ext-real Element of the carrier of R^1
[.P,p2.] is V128() V129() V130() closed Element of bool REAL
T is TopSpace-like TopStruct
the carrier of T is set
bool the carrier of T is non empty set
bool (bool the carrier of T) is non empty set
{} T is empty V36() V40() open closed connected V128() V129() V130() V131() V132() V133() V134() Element of bool the carrier of T
{({} T)} is non empty V36() V40() set
F is Element of bool (bool the carrier of T)
P is Element of bool the carrier of T
P is Element of bool the carrier of T