begin
begin
theorem
for
T being ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace)
for
a,
b,
c being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
for
f being ( ( ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V82()
normal T_3 T_4 connected compact locally_connected V211()
V246()
pathwise_connected pseudocompact )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V211() )
TopStruct ) ) : ( ( ) ( non
empty V166()
V167()
V168() )
set )
-defined the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Path of
a : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ,
b : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) )
for
g being ( ( ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V82()
normal T_3 T_4 connected compact locally_connected V211()
V246()
pathwise_connected pseudocompact )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V211() )
TopStruct ) ) : ( ( ) ( non
empty V166()
V167()
V168() )
set )
-defined the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Path of
b : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ,
c : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ) st
a : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ,
b : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
are_connected &
b : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ,
c : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
are_connected holds
rng f : ( ( ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V82()
normal T_3 T_4 connected compact locally_connected V211()
V246()
pathwise_connected pseudocompact )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V211() )
TopStruct ) ) : ( ( ) ( non
empty V166()
V167()
V168() )
set )
-defined the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Path of
b2 : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ,
b3 : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty )
Element of
bool the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
c= rng (f : ( ( ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 V82() normal T_3 T_4 connected compact locally_connected V211() V246() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 V211() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Path of b2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) + g : ( ( ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 V82() normal T_3 T_4 connected compact locally_connected V211() V246() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 V211() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Path of b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) : ( ( ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V82()
normal T_3 T_4 connected compact locally_connected V211()
V246()
pathwise_connected pseudocompact )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V211() )
TopStruct ) ) : ( ( ) ( non
empty V166()
V167()
V168() )
set )
-defined the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Path of
b2 : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ,
b4 : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty )
Element of
bool the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ;
theorem
for
T being ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace)
for
a,
b,
c being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
for
f being ( ( ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V82()
normal T_3 T_4 connected compact locally_connected V211()
V246()
pathwise_connected pseudocompact )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V211() )
TopStruct ) ) : ( ( ) ( non
empty V166()
V167()
V168() )
set )
-defined the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Path of
b : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ,
c : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) )
for
g being ( ( ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V82()
normal T_3 T_4 connected compact locally_connected V211()
V246()
pathwise_connected pseudocompact )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V211() )
TopStruct ) ) : ( ( ) ( non
empty V166()
V167()
V168() )
set )
-defined the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Path of
a : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ,
b : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ) st
a : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ,
b : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
are_connected &
b : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ,
c : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
are_connected holds
rng f : ( ( ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V82()
normal T_3 T_4 connected compact locally_connected V211()
V246()
pathwise_connected pseudocompact )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V211() )
TopStruct ) ) : ( ( ) ( non
empty V166()
V167()
V168() )
set )
-defined the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Path of
b3 : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ,
b4 : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty )
Element of
bool the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
c= rng (g : ( ( ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 V82() normal T_3 T_4 connected compact locally_connected V211() V246() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 V211() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Path of b2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) + f : ( ( ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 V82() normal T_3 T_4 connected compact locally_connected V211() V246() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 V211() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Path of b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) : ( ( ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V82()
normal T_3 T_4 connected compact locally_connected V211()
V246()
pathwise_connected pseudocompact )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V211() )
TopStruct ) ) : ( ( ) ( non
empty V166()
V167()
V168() )
set )
-defined the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Path of
b2 : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ,
b4 : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty )
Element of
bool the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ;
theorem
for
T being ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace)
for
a,
b,
c being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
for
f being ( ( ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V82()
normal T_3 T_4 connected compact locally_connected V211()
V246()
pathwise_connected pseudocompact )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V211() )
TopStruct ) ) : ( ( ) ( non
empty V166()
V167()
V168() )
set )
-defined the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Path of
a : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ,
b : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) )
for
g being ( ( ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V82()
normal T_3 T_4 connected compact locally_connected V211()
V246()
pathwise_connected pseudocompact )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V211() )
TopStruct ) ) : ( ( ) ( non
empty V166()
V167()
V168() )
set )
-defined the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Path of
b : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ,
c : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ) st
a : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ,
b : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
are_connected &
b : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ,
c : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
are_connected holds
rng (f : ( ( ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 V82() normal T_3 T_4 connected compact locally_connected V211() V246() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 V211() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Path of b2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) + g : ( ( ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 V82() normal T_3 T_4 connected compact locally_connected V211() V246() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 V211() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Path of b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) : ( ( ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V82()
normal T_3 T_4 connected compact locally_connected V211()
V246()
pathwise_connected pseudocompact )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V211() )
TopStruct ) ) : ( ( ) ( non
empty V166()
V167()
V168() )
set )
-defined the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Path of
b2 : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ,
b4 : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty )
Element of
bool the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
= (rng f : ( ( ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 V82() normal T_3 T_4 connected compact locally_connected V211() V246() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 V211() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Path of b2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non
empty )
Element of
bool the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
\/ (rng g : ( ( ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 V82() normal T_3 T_4 connected compact locally_connected V211() V246() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 V211() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Path of b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non
empty )
Element of
bool the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
Element of
bool the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ;
theorem
for
T being ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace)
for
a,
b,
c,
d being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
for
f being ( ( ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V82()
normal T_3 T_4 connected compact locally_connected V211()
V246()
pathwise_connected pseudocompact )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V211() )
TopStruct ) ) : ( ( ) ( non
empty V166()
V167()
V168() )
set )
-defined the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Path of
a : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ,
b : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) )
for
g being ( ( ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V82()
normal T_3 T_4 connected compact locally_connected V211()
V246()
pathwise_connected pseudocompact )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V211() )
TopStruct ) ) : ( ( ) ( non
empty V166()
V167()
V168() )
set )
-defined the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Path of
b : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ,
c : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) )
for
h being ( ( ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V82()
normal T_3 T_4 connected compact locally_connected V211()
V246()
pathwise_connected pseudocompact )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V211() )
TopStruct ) ) : ( ( ) ( non
empty V166()
V167()
V168() )
set )
-defined the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Path of
c : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ,
d : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ) st
a : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ,
b : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
are_connected &
b : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ,
c : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
are_connected &
c : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ,
d : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
are_connected holds
rng ((f : ( ( ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 V82() normal T_3 T_4 connected compact locally_connected V211() V246() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 V211() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Path of b2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) + g : ( ( ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 V82() normal T_3 T_4 connected compact locally_connected V211() V246() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 V211() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Path of b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 V82() normal T_3 T_4 connected compact locally_connected V211() V246() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 V211() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Path of b2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) + h : ( ( ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 V82() normal T_3 T_4 connected compact locally_connected V211() V246() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 V211() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Path of b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b5 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) : ( ( ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V82()
normal T_3 T_4 connected compact locally_connected V211()
V246()
pathwise_connected pseudocompact )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V211() )
TopStruct ) ) : ( ( ) ( non
empty V166()
V167()
V168() )
set )
-defined the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Path of
b2 : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ,
b5 : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty )
Element of
bool the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
= ((rng f : ( ( ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 V82() normal T_3 T_4 connected compact locally_connected V211() V246() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 V211() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Path of b2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) \/ (rng g : ( ( ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 V82() normal T_3 T_4 connected compact locally_connected V211() V246() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 V211() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Path of b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non
empty )
Element of
bool the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
\/ (rng h : ( ( ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 V82() normal T_3 T_4 connected compact locally_connected V211() V246() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 V211() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total ) Path of b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b5 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non
empty )
Element of
bool the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
Element of
bool the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ;
theorem
for
T being ( ( non
empty TopSpace-like pathwise_connected ) ( non
empty TopSpace-like connected pathwise_connected )
TopSpace)
for
a,
b,
c,
d being ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) )
for
f being ( ( ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V82()
normal T_3 T_4 connected compact locally_connected V211()
V246()
pathwise_connected pseudocompact )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V211() )
TopStruct ) ) : ( ( ) ( non
empty V166()
V167()
V168() )
set )
-defined the
carrier of
b1 : ( ( non
empty TopSpace-like pathwise_connected ) ( non
empty TopSpace-like connected pathwise_connected )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total continuous )
Path of
a : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ,
b : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) )
for
g being ( ( ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V82()
normal T_3 T_4 connected compact locally_connected V211()
V246()
pathwise_connected pseudocompact )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V211() )
TopStruct ) ) : ( ( ) ( non
empty V166()
V167()
V168() )
set )
-defined the
carrier of
b1 : ( ( non
empty TopSpace-like pathwise_connected ) ( non
empty TopSpace-like connected pathwise_connected )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total continuous )
Path of
b : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ,
c : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) )
for
h being ( ( ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V82()
normal T_3 T_4 connected compact locally_connected V211()
V246()
pathwise_connected pseudocompact )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V211() )
TopStruct ) ) : ( ( ) ( non
empty V166()
V167()
V168() )
set )
-defined the
carrier of
b1 : ( ( non
empty TopSpace-like pathwise_connected ) ( non
empty TopSpace-like connected pathwise_connected )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total continuous )
Path of
c : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ,
d : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ) holds
rng ((f : ( ( ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 V82() normal T_3 T_4 connected compact locally_connected V211() V246() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 V211() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like pathwise_connected ) ( non empty TopSpace-like connected pathwise_connected ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total continuous ) Path of b2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) + g : ( ( ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 V82() normal T_3 T_4 connected compact locally_connected V211() V246() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 V211() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like pathwise_connected ) ( non empty TopSpace-like connected pathwise_connected ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total continuous ) Path of b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 V82() normal T_3 T_4 connected compact locally_connected V211() V246() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 V211() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like pathwise_connected ) ( non empty TopSpace-like connected pathwise_connected ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total continuous ) Path of b2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) + h : ( ( ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 V82() normal T_3 T_4 connected compact locally_connected V211() V246() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 V211() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like pathwise_connected ) ( non empty TopSpace-like connected pathwise_connected ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total continuous ) Path of b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b5 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) : ( ( ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V82()
normal T_3 T_4 connected compact locally_connected V211()
V246()
pathwise_connected pseudocompact )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V211() )
TopStruct ) ) : ( ( ) ( non
empty V166()
V167()
V168() )
set )
-defined the
carrier of
b1 : ( ( non
empty TopSpace-like pathwise_connected ) ( non
empty TopSpace-like connected pathwise_connected )
TopSpace) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total continuous )
Path of
b2 : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ,
b5 : ( ( ) ( )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty )
Element of
bool the
carrier of
b1 : ( ( non
empty TopSpace-like pathwise_connected ) ( non
empty TopSpace-like connected pathwise_connected )
TopSpace) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
= ((rng f : ( ( ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 V82() normal T_3 T_4 connected compact locally_connected V211() V246() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 V211() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like pathwise_connected ) ( non empty TopSpace-like connected pathwise_connected ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total continuous ) Path of b2 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like pathwise_connected ) ( non empty TopSpace-like connected pathwise_connected ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) \/ (rng g : ( ( ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 V82() normal T_3 T_4 connected compact locally_connected V211() V246() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 V211() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like pathwise_connected ) ( non empty TopSpace-like connected pathwise_connected ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total continuous ) Path of b3 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non empty ) Element of bool the carrier of b1 : ( ( non empty TopSpace-like pathwise_connected ) ( non empty TopSpace-like connected pathwise_connected ) TopSpace) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non
empty )
Element of
bool the
carrier of
b1 : ( ( non
empty TopSpace-like pathwise_connected ) ( non
empty TopSpace-like connected pathwise_connected )
TopSpace) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) )
\/ (rng h : ( ( ) ( Relation-like the carrier of I[01] : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 V82() normal T_3 T_4 connected compact locally_connected V211() V246() pathwise_connected pseudocompact ) SubSpace of R^1 : ( ( TopSpace-like ) ( non empty strict TopSpace-like T_0 T_1 T_2 V211() ) TopStruct ) ) : ( ( ) ( non empty V166() V167() V168() ) set ) -defined the carrier of b1 : ( ( non empty TopSpace-like pathwise_connected ) ( non empty TopSpace-like connected pathwise_connected ) TopSpace) : ( ( ) ( non empty ) set ) -valued Function-like non empty total quasi_total continuous ) Path of b4 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ,b5 : ( ( ) ( ) Point of ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( non
empty )
Element of
bool the
carrier of
b1 : ( ( non
empty TopSpace-like pathwise_connected ) ( non
empty TopSpace-like connected pathwise_connected )
TopSpace) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( non
empty )
Element of
bool the
carrier of
b1 : ( ( non
empty TopSpace-like pathwise_connected ) ( non
empty TopSpace-like connected pathwise_connected )
TopSpace) : ( ( ) ( non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ;
theorem
for
n being ( ( ) (
ordinal natural complex ext-real non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) )
for
p1,
p2 being ( ( ) (
Relation-like Function-like V49(
b1 : ( ( ) (
ordinal natural complex ext-real non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Point of ( ( ) (
functional non
empty )
set ) ) ex
F being ( ( ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V82()
normal T_3 T_4 connected compact locally_connected V211()
V246()
pathwise_connected pseudocompact )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V211() )
TopStruct ) ) : ( ( ) ( non
empty V166()
V167()
V168() )
set )
-defined the
carrier of
(TOP-REAL b1 : ( ( ) ( ordinal natural complex ext-real non negative real V33() V119() V166() V167() V168() V169() V170() V171() bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set )
-valued Function-like non
empty total quasi_total continuous )
Path of
p1 : ( ( ) (
Relation-like Function-like V49(
b1 : ( ( ) (
ordinal natural complex ext-real non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Point of ( ( ) (
functional non
empty )
set ) ) ,
p2 : ( ( ) (
Relation-like Function-like V49(
b1 : ( ( ) (
ordinal natural complex ext-real non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Point of ( ( ) (
functional non
empty )
set ) ) ) ex
f being ( (
Function-like quasi_total ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V82()
normal T_3 T_4 connected compact locally_connected V211()
V246()
pathwise_connected pseudocompact )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V211() )
TopStruct ) ) : ( ( ) ( non
empty V166()
V167()
V168() )
set )
-defined the
carrier of
((TOP-REAL b1 : ( ( ) ( ordinal natural complex ext-real non negative real V33() V119() V166() V167() V168() V169() V170() V171() bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) | (LSeg (b2 : ( ( ) ( Relation-like Function-like V49(b1 : ( ( ) ( ordinal natural complex ext-real non negative real V33() V119() V166() V167() V168() V169() V170() V171() bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Point of ( ( ) ( functional non empty ) set ) ) ,b3 : ( ( ) ( Relation-like Function-like V49(b1 : ( ( ) ( ordinal natural complex ext-real non negative real V33() V119() V166() V167() V168() V169() V170() V171() bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Point of ( ( ) ( functional non empty ) set ) ) )) : ( ( ) ( functional closed compact bounded ) Element of bool the carrier of (TOP-REAL b1 : ( ( ) ( ordinal natural complex ext-real non negative real V33() V119() V166() V167() V168() V169() V170() V171() bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( (
strict ) (
strict TopSpace-like T_0 T_1 T_2 )
SubSpace of
TOP-REAL b1 : ( ( ) (
ordinal natural complex ext-real non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) ) : ( ( ) ( )
set )
-valued Function-like quasi_total )
Function of ( ( ) ( non
empty V166()
V167()
V168() )
set ) , ( ( ) ( )
set ) ) st
(
rng f : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V82()
normal T_3 T_4 connected compact locally_connected V211()
V246()
pathwise_connected pseudocompact )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V211() )
TopStruct ) ) : ( ( ) ( non
empty V166()
V167()
V168() )
set )
-defined the
carrier of
((TOP-REAL b1 : ( ( ) ( ordinal natural complex ext-real non negative real V33() V119() V166() V167() V168() V169() V170() V171() bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) | (LSeg (b2 : ( ( ) ( Relation-like Function-like V49(b1 : ( ( ) ( ordinal natural complex ext-real non negative real V33() V119() V166() V167() V168() V169() V170() V171() bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Point of ( ( ) ( functional non empty ) set ) ) ,b3 : ( ( ) ( Relation-like Function-like V49(b1 : ( ( ) ( ordinal natural complex ext-real non negative real V33() V119() V166() V167() V168() V169() V170() V171() bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Point of ( ( ) ( functional non empty ) set ) ) )) : ( ( ) ( functional closed compact bounded ) Element of bool the carrier of (TOP-REAL b1 : ( ( ) ( ordinal natural complex ext-real non negative real V33() V119() V166() V167() V168() V169() V170() V171() bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( (
strict ) (
strict TopSpace-like T_0 T_1 T_2 )
SubSpace of
TOP-REAL b1 : ( ( ) (
ordinal natural complex ext-real non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) ) : ( ( ) ( )
set )
-valued Function-like quasi_total )
Function of ( ( ) ( non
empty V166()
V167()
V168() )
set ) , ( ( ) ( )
set ) ) : ( ( ) ( )
Element of
bool the
carrier of
((TOP-REAL b1 : ( ( ) ( ordinal natural complex ext-real non negative real V33() V119() V166() V167() V168() V169() V170() V171() bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) | (LSeg (b2 : ( ( ) ( Relation-like Function-like V49(b1 : ( ( ) ( ordinal natural complex ext-real non negative real V33() V119() V166() V167() V168() V169() V170() V171() bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Point of ( ( ) ( functional non empty ) set ) ) ,b3 : ( ( ) ( Relation-like Function-like V49(b1 : ( ( ) ( ordinal natural complex ext-real non negative real V33() V119() V166() V167() V168() V169() V170() V171() bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Point of ( ( ) ( functional non empty ) set ) ) )) : ( ( ) ( functional closed compact bounded ) Element of bool the carrier of (TOP-REAL b1 : ( ( ) ( ordinal natural complex ext-real non negative real V33() V119() V166() V167() V168() V169() V170() V171() bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( (
strict ) (
strict TopSpace-like T_0 T_1 T_2 )
SubSpace of
TOP-REAL b1 : ( ( ) (
ordinal natural complex ext-real non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) ) : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) )
= LSeg (
p1 : ( ( ) (
Relation-like Function-like V49(
b1 : ( ( ) (
ordinal natural complex ext-real non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Point of ( ( ) (
functional non
empty )
set ) ) ,
p2 : ( ( ) (
Relation-like Function-like V49(
b1 : ( ( ) (
ordinal natural complex ext-real non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Point of ( ( ) (
functional non
empty )
set ) ) ) : ( ( ) (
functional closed compact bounded )
Element of
bool the
carrier of
(TOP-REAL b1 : ( ( ) ( ordinal natural complex ext-real non negative real V33() V119() V166() V167() V168() V169() V170() V171() bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) : ( ( ) ( non
empty )
set ) ) &
F : ( ( ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V82()
normal T_3 T_4 connected compact locally_connected V211()
V246()
pathwise_connected pseudocompact )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V211() )
TopStruct ) ) : ( ( ) ( non
empty V166()
V167()
V168() )
set )
-defined the
carrier of
(TOP-REAL b1 : ( ( ) ( ordinal natural complex ext-real non negative real V33() V119() V166() V167() V168() V169() V170() V171() bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set )
-valued Function-like non
empty total quasi_total continuous )
Path of
b2 : ( ( ) (
Relation-like Function-like V49(
b1 : ( ( ) (
ordinal natural complex ext-real non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Point of ( ( ) (
functional non
empty )
set ) ) ,
b3 : ( ( ) (
Relation-like Function-like V49(
b1 : ( ( ) (
ordinal natural complex ext-real non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Point of ( ( ) (
functional non
empty )
set ) ) )
= f : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
I[01] : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V82()
normal T_3 T_4 connected compact locally_connected V211()
V246()
pathwise_connected pseudocompact )
SubSpace of
R^1 : ( (
TopSpace-like ) ( non
empty strict TopSpace-like T_0 T_1 T_2 V211() )
TopStruct ) ) : ( ( ) ( non
empty V166()
V167()
V168() )
set )
-defined the
carrier of
((TOP-REAL b1 : ( ( ) ( ordinal natural complex ext-real non negative real V33() V119() V166() V167() V168() V169() V170() V171() bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) | (LSeg (b2 : ( ( ) ( Relation-like Function-like V49(b1 : ( ( ) ( ordinal natural complex ext-real non negative real V33() V119() V166() V167() V168() V169() V170() V171() bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Point of ( ( ) ( functional non empty ) set ) ) ,b3 : ( ( ) ( Relation-like Function-like V49(b1 : ( ( ) ( ordinal natural complex ext-real non negative real V33() V119() V166() V167() V168() V169() V170() V171() bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Point of ( ( ) ( functional non empty ) set ) ) )) : ( ( ) ( functional closed compact bounded ) Element of bool the carrier of (TOP-REAL b1 : ( ( ) ( ordinal natural complex ext-real non negative real V33() V119() V166() V167() V168() V169() V170() V171() bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( (
strict ) (
strict TopSpace-like T_0 T_1 T_2 )
SubSpace of
TOP-REAL b1 : ( ( ) (
ordinal natural complex ext-real non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) ) : ( ( ) ( )
set )
-valued Function-like quasi_total )
Function of ( ( ) ( non
empty V166()
V167()
V168() )
set ) , ( ( ) ( )
set ) ) ) ;
begin
theorem
for
a,
b,
c,
d being ( (
real ) (
complex ext-real real )
number ) holds
(closed_inside_of_rectangle (a : ( ( real ) ( complex ext-real real ) number ) ,b : ( ( real ) ( complex ext-real real ) number ) ,c : ( ( real ) ( complex ext-real real ) number ) ,d : ( ( real ) ( complex ext-real real ) number ) )) : ( ( ) (
functional closed connected convex )
Element of
bool the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) : ( ( ) ( non
empty )
set ) )
/\ (inside_of_rectangle (a : ( ( real ) ( complex ext-real real ) number ) ,b : ( ( real ) ( complex ext-real real ) number ) ,c : ( ( real ) ( complex ext-real real ) number ) ,d : ( ( real ) ( complex ext-real real ) number ) )) : ( ( ) (
functional )
Element of
bool the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
functional )
Element of
bool the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) : ( ( ) ( non
empty )
set ) )
= inside_of_rectangle (
a : ( (
real ) (
complex ext-real real )
number ) ,
b : ( (
real ) (
complex ext-real real )
number ) ,
c : ( (
real ) (
complex ext-real real )
number ) ,
d : ( (
real ) (
complex ext-real real )
number ) ) : ( ( ) (
functional )
Element of
bool the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ;
theorem
for
a,
b,
c,
d being ( (
real ) (
complex ext-real real )
number ) st
a : ( (
real ) (
complex ext-real real )
number )
<= b : ( (
real ) (
complex ext-real real )
number ) &
c : ( (
real ) (
complex ext-real real )
number )
<= d : ( (
real ) (
complex ext-real real )
number ) holds
(closed_inside_of_rectangle (a : ( ( real ) ( complex ext-real real ) number ) ,b : ( ( real ) ( complex ext-real real ) number ) ,c : ( ( real ) ( complex ext-real real ) number ) ,d : ( ( real ) ( complex ext-real real ) number ) )) : ( ( ) (
functional closed connected convex )
Element of
bool the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) : ( ( ) ( non
empty )
set ) )
\ (inside_of_rectangle (a : ( ( real ) ( complex ext-real real ) number ) ,b : ( ( real ) ( complex ext-real real ) number ) ,c : ( ( real ) ( complex ext-real real ) number ) ,d : ( ( real ) ( complex ext-real real ) number ) )) : ( ( ) (
functional )
Element of
bool the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) : ( ( ) ( non
empty )
set ) ) : ( ( ) (
functional )
Element of
bool the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) : ( ( ) ( non
empty )
set ) )
= rectangle (
a : ( (
real ) (
complex ext-real real )
number ) ,
b : ( (
real ) (
complex ext-real real )
number ) ,
c : ( (
real ) (
complex ext-real real )
number ) ,
d : ( (
real ) (
complex ext-real real )
number ) ) : ( ( ) (
functional non
empty proper closed compact bounded )
Element of
bool the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ;
theorem
for
a,
b,
c,
d being ( (
real ) (
complex ext-real real )
number )
for
p1,
p2 being ( ( ) (
Relation-like Function-like V49(2 : ( ( ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Point of ( ( ) (
functional non
empty )
set ) )
for
P being ( ( ) (
functional )
Subset of ) st
a : ( (
real ) (
complex ext-real real )
number )
< b : ( (
real ) (
complex ext-real real )
number ) &
c : ( (
real ) (
complex ext-real real )
number )
< d : ( (
real ) (
complex ext-real real )
number ) &
p1 : ( ( ) (
Relation-like Function-like V49(2 : ( ( ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Point of ( ( ) (
functional non
empty )
set ) )
in closed_inside_of_rectangle (
a : ( (
real ) (
complex ext-real real )
number ) ,
b : ( (
real ) (
complex ext-real real )
number ) ,
c : ( (
real ) (
complex ext-real real )
number ) ,
d : ( (
real ) (
complex ext-real real )
number ) ) : ( ( ) (
functional closed connected convex )
Element of
bool the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) : ( ( ) ( non
empty )
set ) ) & not
p2 : ( ( ) (
Relation-like Function-like V49(2 : ( ( ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Point of ( ( ) (
functional non
empty )
set ) )
in closed_inside_of_rectangle (
a : ( (
real ) (
complex ext-real real )
number ) ,
b : ( (
real ) (
complex ext-real real )
number ) ,
c : ( (
real ) (
complex ext-real real )
number ) ,
d : ( (
real ) (
complex ext-real real )
number ) ) : ( ( ) (
functional closed connected convex )
Element of
bool the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) : ( ( ) ( non
empty )
set ) ) &
P : ( ( ) (
functional )
Subset of )
is_an_arc_of p1 : ( ( ) (
Relation-like Function-like V49(2 : ( ( ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Point of ( ( ) (
functional non
empty )
set ) ) ,
p2 : ( ( ) (
Relation-like Function-like V49(2 : ( ( ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Point of ( ( ) (
functional non
empty )
set ) ) holds
Segment (
P : ( ( ) (
functional )
Subset of ) ,
p1 : ( ( ) (
Relation-like Function-like V49(2 : ( ( ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Point of ( ( ) (
functional non
empty )
set ) ) ,
p2 : ( ( ) (
Relation-like Function-like V49(2 : ( ( ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Point of ( ( ) (
functional non
empty )
set ) ) ,
p1 : ( ( ) (
Relation-like Function-like V49(2 : ( ( ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Point of ( ( ) (
functional non
empty )
set ) ) ,
(First_Point (P : ( ( ) ( functional ) Subset of ) ,p1 : ( ( ) ( Relation-like Function-like V49(2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Point of ( ( ) ( functional non empty ) set ) ) ,p2 : ( ( ) ( Relation-like Function-like V49(2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Point of ( ( ) ( functional non empty ) set ) ) ,(rectangle (a : ( ( real ) ( complex ext-real real ) number ) ,b : ( ( real ) ( complex ext-real real ) number ) ,c : ( ( real ) ( complex ext-real real ) number ) ,d : ( ( real ) ( complex ext-real real ) number ) )) : ( ( ) ( functional non empty proper closed compact bounded ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) : ( ( ) ( non empty ) set ) ) )) : ( ( ) (
Relation-like Function-like V49(2 : ( ( ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) ) : ( ( ) (
functional )
Element of
bool the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) : ( ( ) ( non
empty )
set ) )
c= closed_inside_of_rectangle (
a : ( (
real ) (
complex ext-real real )
number ) ,
b : ( (
real ) (
complex ext-real real )
number ) ,
c : ( (
real ) (
complex ext-real real )
number ) ,
d : ( (
real ) (
complex ext-real real )
number ) ) : ( ( ) (
functional closed connected convex )
Element of
bool the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ;
begin
theorem
for
n being ( ( non
empty ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) )
for
o,
p being ( ( ) (
Relation-like Function-like V49(
b1 : ( ( non
empty ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Point of ( ( ) (
functional non
empty )
set ) )
for
r being ( (
positive real ) ( non
empty complex ext-real positive non
negative real )
number ) st
p : ( ( ) (
Relation-like Function-like V49(
b1 : ( ( non
empty ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Point of ( ( ) (
functional non
empty )
set ) )
in Ball (
o : ( ( ) (
Relation-like Function-like V49(
b1 : ( ( non
empty ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Point of ( ( ) (
functional non
empty )
set ) ) ,
r : ( (
positive real ) ( non
empty complex ext-real positive non
negative real )
number ) ) : ( ( ) (
functional non
empty proper open connected bounded convex )
Element of
bool the
carrier of
(TOP-REAL b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) : ( ( ) ( non
empty )
set ) ) holds
(DiskProj (o : ( ( ) ( Relation-like Function-like V49(b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Point of ( ( ) ( functional non empty ) set ) ) ,r : ( ( positive real ) ( non empty complex ext-real positive non negative real ) number ) ,p : ( ( ) ( Relation-like Function-like V49(b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Point of ( ( ) ( functional non empty ) set ) ) )) : ( (
Function-like quasi_total ) (
Relation-like the
carrier of
((TOP-REAL b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) | ((cl_Ball (b2 : ( ( ) ( Relation-like Function-like V49(b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Point of ( ( ) ( functional non empty ) set ) ) ,b4 : ( ( positive real ) ( non empty complex ext-real positive non negative real ) number ) )) : ( ( ) ( functional non empty proper closed connected bounded convex ) Element of bool the carrier of (TOP-REAL b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) : ( ( ) ( non empty ) set ) ) \ {b3 : ( ( ) ( Relation-like Function-like V49(b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Point of ( ( ) ( functional non empty ) set ) ) } : ( ( ) ( functional non empty proper closed compact bounded ) Element of bool the carrier of (TOP-REAL b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional non empty ) Element of bool the carrier of (TOP-REAL b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( (
strict ) ( non
empty strict TopSpace-like T_0 T_1 T_2 )
SubSpace of
TOP-REAL b1 : ( ( non
empty ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
(Tcircle (b2 : ( ( ) ( Relation-like Function-like V49(b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Point of ( ( ) ( functional non empty ) set ) ) ,b4 : ( ( positive real ) ( non empty complex ext-real positive non negative real ) number ) )) : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 )
SubSpace of
TOP-REAL b1 : ( ( non
empty ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) ) : ( ( ) ( non
empty )
set )
-valued Function-like non
empty total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
| (Sphere (o : ( ( ) ( Relation-like Function-like V49(b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Point of ( ( ) ( functional non empty ) set ) ) ,r : ( ( positive real ) ( non empty complex ext-real positive non negative real ) number ) )) : ( ( ) (
functional non
empty proper closed bounded )
Element of
bool the
carrier of
(TOP-REAL b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) : ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
Relation-like Sphere (
b2 : ( ( ) (
Relation-like Function-like V49(
b1 : ( ( non
empty ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Point of ( ( ) (
functional non
empty )
set ) ) ,
b4 : ( (
positive real ) ( non
empty complex ext-real positive non
negative real )
number ) ) : ( ( ) (
functional non
empty proper closed bounded )
Element of
bool the
carrier of
(TOP-REAL b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) : ( ( ) ( non
empty )
set ) )
-defined the
carrier of
((TOP-REAL b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) | ((cl_Ball (b2 : ( ( ) ( Relation-like Function-like V49(b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Point of ( ( ) ( functional non empty ) set ) ) ,b4 : ( ( positive real ) ( non empty complex ext-real positive non negative real ) number ) )) : ( ( ) ( functional non empty proper closed connected bounded convex ) Element of bool the carrier of (TOP-REAL b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) : ( ( ) ( non empty ) set ) ) \ {b3 : ( ( ) ( Relation-like Function-like V49(b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Point of ( ( ) ( functional non empty ) set ) ) } : ( ( ) ( functional non empty proper closed compact bounded ) Element of bool the carrier of (TOP-REAL b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional non empty ) Element of bool the carrier of (TOP-REAL b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( (
strict ) ( non
empty strict TopSpace-like T_0 T_1 T_2 )
SubSpace of
TOP-REAL b1 : ( ( non
empty ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) ) : ( ( ) ( non
empty )
set )
-defined the
carrier of
(Tcircle (b2 : ( ( ) ( Relation-like Function-like V49(b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Point of ( ( ) ( functional non empty ) set ) ) ,b4 : ( ( positive real ) ( non empty complex ext-real positive non negative real ) number ) )) : ( ( ) ( non
empty strict TopSpace-like T_0 T_1 T_2 )
SubSpace of
TOP-REAL b1 : ( ( non
empty ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) ) : ( ( ) ( non
empty )
set )
-valued Function-like )
Element of
bool [: the carrier of ((TOP-REAL b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) | ((cl_Ball (b2 : ( ( ) ( Relation-like Function-like V49(b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Point of ( ( ) ( functional non empty ) set ) ) ,b4 : ( ( positive real ) ( non empty complex ext-real positive non negative real ) number ) )) : ( ( ) ( functional non empty proper closed connected bounded convex ) Element of bool the carrier of (TOP-REAL b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) : ( ( ) ( non empty ) set ) ) \ {b3 : ( ( ) ( Relation-like Function-like V49(b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Point of ( ( ) ( functional non empty ) set ) ) } : ( ( ) ( functional non empty proper closed compact bounded ) Element of bool the carrier of (TOP-REAL b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( functional non empty ) Element of bool the carrier of (TOP-REAL b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty strict TopSpace-like T_0 T_1 T_2 ) SubSpace of TOP-REAL b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) ) : ( ( ) ( non empty ) set ) , the carrier of (Tcircle (b2 : ( ( ) ( Relation-like Function-like V49(b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Point of ( ( ) ( functional non empty ) set ) ) ,b4 : ( ( positive real ) ( non empty complex ext-real positive non negative real ) number ) )) : ( ( ) ( non empty strict TopSpace-like T_0 T_1 T_2 ) SubSpace of TOP-REAL b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) ) : ( ( ) ( non empty ) set ) :] : ( ( ) (
Relation-like non
empty )
set ) : ( ( ) ( non
empty )
set ) )
= id (Sphere (o : ( ( ) ( Relation-like Function-like V49(b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Point of ( ( ) ( functional non empty ) set ) ) ,r : ( ( positive real ) ( non empty complex ext-real positive non negative real ) number ) )) : ( ( ) (
functional non
empty proper closed bounded )
Element of
bool the
carrier of
(TOP-REAL b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) : ( ( ) ( non
empty )
set ) ) : ( (
total ) (
Relation-like Sphere (
b2 : ( ( ) (
Relation-like Function-like V49(
b1 : ( ( non
empty ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Point of ( ( ) (
functional non
empty )
set ) ) ,
b4 : ( (
positive real ) ( non
empty complex ext-real positive non
negative real )
number ) ) : ( ( ) (
functional non
empty proper closed bounded )
Element of
bool the
carrier of
(TOP-REAL b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) : ( ( ) ( non
empty )
set ) )
-defined Sphere (
b2 : ( ( ) (
Relation-like Function-like V49(
b1 : ( ( non
empty ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Point of ( ( ) (
functional non
empty )
set ) ) ,
b4 : ( (
positive real ) ( non
empty complex ext-real positive non
negative real )
number ) ) : ( ( ) (
functional non
empty proper closed bounded )
Element of
bool the
carrier of
(TOP-REAL b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) : ( ( ) ( non
empty )
set ) )
-valued Function-like one-to-one non
empty total quasi_total )
Element of
bool [:(Sphere (b2 : ( ( ) ( Relation-like Function-like V49(b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Point of ( ( ) ( functional non empty ) set ) ) ,b4 : ( ( positive real ) ( non empty complex ext-real positive non negative real ) number ) )) : ( ( ) ( functional non empty proper closed bounded ) Element of bool the carrier of (TOP-REAL b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) : ( ( ) ( non empty ) set ) ) ,(Sphere (b2 : ( ( ) ( Relation-like Function-like V49(b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Point of ( ( ) ( functional non empty ) set ) ) ,b4 : ( ( positive real ) ( non empty complex ext-real positive non negative real ) number ) )) : ( ( ) ( functional non empty proper closed bounded ) Element of bool the carrier of (TOP-REAL b1 : ( ( non empty ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) : ( ( ) ( non empty ) set ) ) :] : ( ( ) (
Relation-like non
empty )
set ) : ( ( ) ( non
empty )
set ) ) ;
begin
theorem
for
C being ( (
being_simple_closed_curve ) (
functional non
empty closed connected compact bounded being_simple_closed_curve with_the_max_arc )
Simple_closed_curve) st
|[(- 1 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( complex ext-real non positive real ) Element of REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) ) ,0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V42() V166() V167() V168() V169() V172() ) set ) -valued Function-like one-to-one constant functional empty ordinal natural complex ext-real non positive non negative real V33() V119() V156() V157() V158() V159() V166() V167() V168() V169() V170() V171() V172() bounded_below interval ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ]| : ( ( ) (
Relation-like Function-like V49(2 : ( ( ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) ,
|[1 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ,0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V42() V166() V167() V168() V169() V172() ) set ) -valued Function-like one-to-one constant functional empty ordinal natural complex ext-real non positive non negative real V33() V119() V156() V157() V158() V159() V166() V167() V168() V169() V170() V171() V172() bounded_below interval ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ]| : ( ( ) (
Relation-like Function-like V49(2 : ( ( ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) )
realize-max-dist-in C : ( (
being_simple_closed_curve ) (
functional non
empty proper closed connected compact bounded being_simple_closed_curve with_the_max_arc )
Simple_closed_curve) holds
for
Jc,
Jd being ( (
compact with_the_max_arc ) (
functional non
empty proper closed compact bounded with_the_max_arc )
Subset of ) st
Jc : ( (
compact with_the_max_arc ) (
functional non
empty proper closed compact bounded with_the_max_arc )
Subset of )
is_an_arc_of |[(- 1 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( complex ext-real non positive real ) Element of REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) ) ,0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V42() V166() V167() V168() V169() V172() ) set ) -valued Function-like one-to-one constant functional empty ordinal natural complex ext-real non positive non negative real V33() V119() V156() V157() V158() V159() V166() V167() V168() V169() V170() V171() V172() bounded_below interval ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ]| : ( ( ) (
Relation-like Function-like V49(2 : ( ( ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) ,
|[1 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ,0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V42() V166() V167() V168() V169() V172() ) set ) -valued Function-like one-to-one constant functional empty ordinal natural complex ext-real non positive non negative real V33() V119() V156() V157() V158() V159() V166() V167() V168() V169() V170() V171() V172() bounded_below interval ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ]| : ( ( ) (
Relation-like Function-like V49(2 : ( ( ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) &
Jd : ( (
compact with_the_max_arc ) (
functional non
empty proper closed compact bounded with_the_max_arc )
Subset of )
is_an_arc_of |[(- 1 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( complex ext-real non positive real ) Element of REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) ) ,0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V42() V166() V167() V168() V169() V172() ) set ) -valued Function-like one-to-one constant functional empty ordinal natural complex ext-real non positive non negative real V33() V119() V156() V157() V158() V159() V166() V167() V168() V169() V170() V171() V172() bounded_below interval ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ]| : ( ( ) (
Relation-like Function-like V49(2 : ( ( ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) ,
|[1 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ,0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V42() V166() V167() V168() V169() V172() ) set ) -valued Function-like one-to-one constant functional empty ordinal natural complex ext-real non positive non negative real V33() V119() V156() V157() V158() V159() V166() V167() V168() V169() V170() V171() V172() bounded_below interval ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ]| : ( ( ) (
Relation-like Function-like V49(2 : ( ( ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) &
C : ( (
being_simple_closed_curve ) (
functional non
empty proper closed connected compact bounded being_simple_closed_curve with_the_max_arc )
Simple_closed_curve)
= Jc : ( (
compact with_the_max_arc ) (
functional non
empty proper closed compact bounded with_the_max_arc )
Subset of )
\/ Jd : ( (
compact with_the_max_arc ) (
functional non
empty proper closed compact bounded with_the_max_arc )
Subset of ) : ( ( ) (
functional non
empty closed )
Element of
bool the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) : ( ( ) ( non
empty )
set ) ) &
Jc : ( (
compact with_the_max_arc ) (
functional non
empty proper closed compact bounded with_the_max_arc )
Subset of )
/\ Jd : ( (
compact with_the_max_arc ) (
functional non
empty proper closed compact bounded with_the_max_arc )
Subset of ) : ( ( ) (
functional proper closed compact bounded )
Element of
bool the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) : ( ( ) ( non
empty )
set ) )
= {|[(- 1 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( complex ext-real non positive real ) Element of REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) ) ,0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V42() V166() V167() V168() V169() V172() ) set ) -valued Function-like one-to-one constant functional empty ordinal natural complex ext-real non positive non negative real V33() V119() V156() V157() V158() V159() V166() V167() V168() V169() V170() V171() V172() bounded_below interval ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ]| : ( ( ) ( Relation-like Function-like V49(2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) ,|[1 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ,0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V42() V166() V167() V168() V169() V172() ) set ) -valued Function-like one-to-one constant functional empty ordinal natural complex ext-real non positive non negative real V33() V119() V156() V157() V158() V159() V166() V167() V168() V169() V170() V171() V172() bounded_below interval ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ]| : ( ( ) ( Relation-like Function-like V49(2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) } : ( ( ) (
functional non
empty )
Element of
bool the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) : ( ( ) ( non
empty )
set ) ) &
UMP C : ( (
being_simple_closed_curve ) (
functional non
empty proper closed connected compact bounded being_simple_closed_curve with_the_max_arc )
Simple_closed_curve) : ( ( ) (
Relation-like Function-like V49(2 : ( ( ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) )
in Jc : ( (
compact with_the_max_arc ) (
functional non
empty proper closed compact bounded with_the_max_arc )
Subset of ) &
LMP C : ( (
being_simple_closed_curve ) (
functional non
empty proper closed connected compact bounded being_simple_closed_curve with_the_max_arc )
Simple_closed_curve) : ( ( ) (
Relation-like Function-like V49(2 : ( ( ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) )
in Jd : ( (
compact with_the_max_arc ) (
functional non
empty proper closed compact bounded with_the_max_arc )
Subset of ) &
W-bound C : ( (
being_simple_closed_curve ) (
functional non
empty proper closed connected compact bounded being_simple_closed_curve with_the_max_arc )
Simple_closed_curve) : ( ( ) (
complex ext-real real )
Element of
REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) )
= W-bound Jc : ( (
compact with_the_max_arc ) (
functional non
empty proper closed compact bounded with_the_max_arc )
Subset of ) : ( ( ) (
complex ext-real real )
Element of
REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) ) &
E-bound C : ( (
being_simple_closed_curve ) (
functional non
empty proper closed connected compact bounded being_simple_closed_curve with_the_max_arc )
Simple_closed_curve) : ( ( ) (
complex ext-real real )
Element of
REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) )
= E-bound Jc : ( (
compact with_the_max_arc ) (
functional non
empty proper closed compact bounded with_the_max_arc )
Subset of ) : ( ( ) (
complex ext-real real )
Element of
REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) ) holds
for
Ux being ( ( ) (
functional )
Subset of ) st
Ux : ( ( ) (
functional )
Subset of )
= Component_of (Down (((1 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) / 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( complex ext-real non negative real ) Element of REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) ) * ((UMP ((LSeg ((LMP Jc : ( ( compact with_the_max_arc ) ( functional non empty proper closed compact bounded with_the_max_arc ) Subset of ) ) : ( ( ) ( Relation-like Function-like V49(2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) ,|[0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V42() V166() V167() V168() V169() V172() ) set ) -valued Function-like one-to-one constant functional empty ordinal natural complex ext-real non positive non negative real V33() V119() V156() V157() V158() V159() V166() V167() V168() V169() V170() V171() V172() bounded_below interval ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ,(- 3 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( complex ext-real non positive real ) Element of REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) ) ]| : ( ( ) ( Relation-like Function-like V49(2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) )) : ( ( ) ( functional proper closed boundary nowhere_dense connected compact bounded ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) : ( ( ) ( non empty ) set ) ) /\ Jd : ( ( compact with_the_max_arc ) ( functional non empty proper closed compact bounded with_the_max_arc ) Subset of ) ) : ( ( ) ( functional proper closed compact bounded ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like Function-like V49(2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) + (LMP Jc : ( ( compact with_the_max_arc ) ( functional non empty proper closed compact bounded with_the_max_arc ) Subset of ) ) : ( ( ) ( Relation-like Function-like V49(2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) ) : ( ( ) ( Relation-like Function-like V49(2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) ) : ( ( ) ( Relation-like Function-like V49(2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) ,(C : ( ( being_simple_closed_curve ) ( functional non empty proper closed connected compact bounded being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) `) : ( ( ) ( functional open ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) : ( ( ) ( non empty ) set ) ) )) : ( ( ) ( )
Element of the
carrier of
((TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) | (b1 : ( ( being_simple_closed_curve ) ( functional non empty proper closed connected compact bounded being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) `) : ( ( ) ( functional open ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( (
strict ) (
strict TopSpace-like T_0 T_1 T_2 V118(
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) ) )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
Element of
bool the
carrier of
((TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) | (b1 : ( ( being_simple_closed_curve ) ( functional non empty proper closed connected compact bounded being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) `) : ( ( ) ( functional open ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( (
strict ) (
strict TopSpace-like T_0 T_1 T_2 V118(
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) ) )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) ) : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) holds
(
Ux : ( ( ) (
functional )
Subset of )
is_inside_component_of C : ( (
being_simple_closed_curve ) (
functional non
empty proper closed connected compact bounded being_simple_closed_curve with_the_max_arc )
Simple_closed_curve) & ( for
V being ( ( ) (
functional )
Subset of ) st
V : ( ( ) (
functional )
Subset of )
is_inside_component_of C : ( (
being_simple_closed_curve ) (
functional non
empty proper closed connected compact bounded being_simple_closed_curve with_the_max_arc )
Simple_closed_curve) holds
V : ( ( ) (
functional )
Subset of )
= Ux : ( ( ) (
functional )
Subset of ) ) ) ;
theorem
for
C being ( (
being_simple_closed_curve ) (
functional non
empty closed connected compact bounded being_simple_closed_curve with_the_max_arc )
Simple_closed_curve) st
|[(- 1 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( complex ext-real non positive real ) Element of REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) ) ,0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V42() V166() V167() V168() V169() V172() ) set ) -valued Function-like one-to-one constant functional empty ordinal natural complex ext-real non positive non negative real V33() V119() V156() V157() V158() V159() V166() V167() V168() V169() V170() V171() V172() bounded_below interval ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ]| : ( ( ) (
Relation-like Function-like V49(2 : ( ( ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) ,
|[1 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ,0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V42() V166() V167() V168() V169() V172() ) set ) -valued Function-like one-to-one constant functional empty ordinal natural complex ext-real non positive non negative real V33() V119() V156() V157() V158() V159() V166() V167() V168() V169() V170() V171() V172() bounded_below interval ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ]| : ( ( ) (
Relation-like Function-like V49(2 : ( ( ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) )
realize-max-dist-in C : ( (
being_simple_closed_curve ) (
functional non
empty proper closed connected compact bounded being_simple_closed_curve with_the_max_arc )
Simple_closed_curve) holds
for
Jc,
Jd being ( (
compact with_the_max_arc ) (
functional non
empty proper closed compact bounded with_the_max_arc )
Subset of ) st
Jc : ( (
compact with_the_max_arc ) (
functional non
empty proper closed compact bounded with_the_max_arc )
Subset of )
is_an_arc_of |[(- 1 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( complex ext-real non positive real ) Element of REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) ) ,0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V42() V166() V167() V168() V169() V172() ) set ) -valued Function-like one-to-one constant functional empty ordinal natural complex ext-real non positive non negative real V33() V119() V156() V157() V158() V159() V166() V167() V168() V169() V170() V171() V172() bounded_below interval ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ]| : ( ( ) (
Relation-like Function-like V49(2 : ( ( ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) ,
|[1 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ,0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V42() V166() V167() V168() V169() V172() ) set ) -valued Function-like one-to-one constant functional empty ordinal natural complex ext-real non positive non negative real V33() V119() V156() V157() V158() V159() V166() V167() V168() V169() V170() V171() V172() bounded_below interval ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ]| : ( ( ) (
Relation-like Function-like V49(2 : ( ( ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) &
Jd : ( (
compact with_the_max_arc ) (
functional non
empty proper closed compact bounded with_the_max_arc )
Subset of )
is_an_arc_of |[(- 1 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( complex ext-real non positive real ) Element of REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) ) ,0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V42() V166() V167() V168() V169() V172() ) set ) -valued Function-like one-to-one constant functional empty ordinal natural complex ext-real non positive non negative real V33() V119() V156() V157() V158() V159() V166() V167() V168() V169() V170() V171() V172() bounded_below interval ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ]| : ( ( ) (
Relation-like Function-like V49(2 : ( ( ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) ,
|[1 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ,0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V42() V166() V167() V168() V169() V172() ) set ) -valued Function-like one-to-one constant functional empty ordinal natural complex ext-real non positive non negative real V33() V119() V156() V157() V158() V159() V166() V167() V168() V169() V170() V171() V172() bounded_below interval ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ]| : ( ( ) (
Relation-like Function-like V49(2 : ( ( ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) ) &
C : ( (
being_simple_closed_curve ) (
functional non
empty proper closed connected compact bounded being_simple_closed_curve with_the_max_arc )
Simple_closed_curve)
= Jc : ( (
compact with_the_max_arc ) (
functional non
empty proper closed compact bounded with_the_max_arc )
Subset of )
\/ Jd : ( (
compact with_the_max_arc ) (
functional non
empty proper closed compact bounded with_the_max_arc )
Subset of ) : ( ( ) (
functional non
empty closed )
Element of
bool the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) : ( ( ) ( non
empty )
set ) ) &
Jc : ( (
compact with_the_max_arc ) (
functional non
empty proper closed compact bounded with_the_max_arc )
Subset of )
/\ Jd : ( (
compact with_the_max_arc ) (
functional non
empty proper closed compact bounded with_the_max_arc )
Subset of ) : ( ( ) (
functional proper closed compact bounded )
Element of
bool the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) : ( ( ) ( non
empty )
set ) )
= {|[(- 1 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( complex ext-real non positive real ) Element of REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) ) ,0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V42() V166() V167() V168() V169() V172() ) set ) -valued Function-like one-to-one constant functional empty ordinal natural complex ext-real non positive non negative real V33() V119() V156() V157() V158() V159() V166() V167() V168() V169() V170() V171() V172() bounded_below interval ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ]| : ( ( ) ( Relation-like Function-like V49(2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) ,|[1 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ,0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V42() V166() V167() V168() V169() V172() ) set ) -valued Function-like one-to-one constant functional empty ordinal natural complex ext-real non positive non negative real V33() V119() V156() V157() V158() V159() V166() V167() V168() V169() V170() V171() V172() bounded_below interval ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ]| : ( ( ) ( Relation-like Function-like V49(2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) } : ( ( ) (
functional non
empty )
Element of
bool the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) : ( ( ) ( non
empty )
set ) ) &
UMP C : ( (
being_simple_closed_curve ) (
functional non
empty proper closed connected compact bounded being_simple_closed_curve with_the_max_arc )
Simple_closed_curve) : ( ( ) (
Relation-like Function-like V49(2 : ( ( ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) )
in Jc : ( (
compact with_the_max_arc ) (
functional non
empty proper closed compact bounded with_the_max_arc )
Subset of ) &
LMP C : ( (
being_simple_closed_curve ) (
functional non
empty proper closed connected compact bounded being_simple_closed_curve with_the_max_arc )
Simple_closed_curve) : ( ( ) (
Relation-like Function-like V49(2 : ( ( ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) )
V50()
V156()
V157()
V158() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) )
in Jd : ( (
compact with_the_max_arc ) (
functional non
empty proper closed compact bounded with_the_max_arc )
Subset of ) &
W-bound C : ( (
being_simple_closed_curve ) (
functional non
empty proper closed connected compact bounded being_simple_closed_curve with_the_max_arc )
Simple_closed_curve) : ( ( ) (
complex ext-real real )
Element of
REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) )
= W-bound Jc : ( (
compact with_the_max_arc ) (
functional non
empty proper closed compact bounded with_the_max_arc )
Subset of ) : ( ( ) (
complex ext-real real )
Element of
REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) ) &
E-bound C : ( (
being_simple_closed_curve ) (
functional non
empty proper closed connected compact bounded being_simple_closed_curve with_the_max_arc )
Simple_closed_curve) : ( ( ) (
complex ext-real real )
Element of
REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) )
= E-bound Jc : ( (
compact with_the_max_arc ) (
functional non
empty proper closed compact bounded with_the_max_arc )
Subset of ) : ( ( ) (
complex ext-real real )
Element of
REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) ) holds
BDD C : ( (
being_simple_closed_curve ) (
functional non
empty proper closed connected compact bounded being_simple_closed_curve with_the_max_arc )
Simple_closed_curve) : ( ( ) (
functional open )
Element of
bool the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) : ( ( ) (
functional non
empty )
set ) : ( ( ) ( non
empty )
set ) )
= Component_of (Down (((1 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) / 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( complex ext-real non negative real ) Element of REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) ) * ((UMP ((LSeg ((LMP Jc : ( ( compact with_the_max_arc ) ( functional non empty proper closed compact bounded with_the_max_arc ) Subset of ) ) : ( ( ) ( Relation-like Function-like V49(2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) ,|[0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V42() V166() V167() V168() V169() V172() ) set ) -valued Function-like one-to-one constant functional empty ordinal natural complex ext-real non positive non negative real V33() V119() V156() V157() V158() V159() V166() V167() V168() V169() V170() V171() V172() bounded_below interval ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ,(- 3 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( ) ( complex ext-real non positive real ) Element of REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) ) ]| : ( ( ) ( Relation-like Function-like V49(2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) )) : ( ( ) ( functional proper closed boundary nowhere_dense connected compact bounded ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) : ( ( ) ( non empty ) set ) ) /\ Jd : ( ( compact with_the_max_arc ) ( functional non empty proper closed compact bounded with_the_max_arc ) Subset of ) ) : ( ( ) ( functional proper closed compact bounded ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( Relation-like Function-like V49(2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) + (LMP Jc : ( ( compact with_the_max_arc ) ( functional non empty proper closed compact bounded with_the_max_arc ) Subset of ) ) : ( ( ) ( Relation-like Function-like V49(2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) ) : ( ( ) ( Relation-like Function-like V49(2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) ) : ( ( ) ( Relation-like Function-like V49(2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) V50() V156() V157() V158() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) ) ,(C : ( ( being_simple_closed_curve ) ( functional non empty proper closed connected compact bounded being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) `) : ( ( ) ( functional open ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) : ( ( ) ( non empty ) set ) ) )) : ( ( ) ( )
Element of the
carrier of
((TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) | (b1 : ( ( being_simple_closed_curve ) ( functional non empty proper closed connected compact bounded being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) `) : ( ( ) ( functional open ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( (
strict ) (
strict TopSpace-like T_0 T_1 T_2 V118(
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) ) )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
Element of
bool the
carrier of
((TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) | (b1 : ( ( being_simple_closed_curve ) ( functional non empty proper closed connected compact bounded being_simple_closed_curve with_the_max_arc ) Simple_closed_curve) `) : ( ( ) ( functional open ) Element of bool the carrier of (TOP-REAL 2 : ( ( ) ( non empty ordinal natural complex ext-real positive non negative real V33() V119() V166() V167() V168() V169() V170() V171() left_end bounded_below ) Element of NAT : ( ( ) ( V166() V167() V168() V169() V170() V171() V172() V200() bounded_below ) Element of bool REAL : ( ( ) ( non empty V42() V166() V167() V168() V172() V200() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 connected V132() V178() V179() V180() V181() V182() V183() V184() strict add-continuous Mult-continuous pathwise_connected ) RLTopStruct ) : ( ( ) ( functional non empty ) set ) : ( ( ) ( non empty ) set ) ) ) : ( (
strict ) (
strict TopSpace-like T_0 T_1 T_2 V118(
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) ) )
SubSpace of
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural complex ext-real positive non
negative real V33()
V119()
V166()
V167()
V168()
V169()
V170()
V171()
left_end bounded_below )
Element of
NAT : ( ( ) (
V166()
V167()
V168()
V169()
V170()
V171()
V172()
V200()
bounded_below )
Element of
bool REAL : ( ( ) ( non
empty V42()
V166()
V167()
V168()
V172()
V200() non
bounded_below non
bounded_above interval )
set ) : ( ( ) ( non
empty )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 connected V132()
V178()
V179()
V180()
V181()
V182()
V183()
V184()
strict add-continuous Mult-continuous pathwise_connected )
RLTopStruct ) ) : ( ( ) ( )
set ) : ( ( ) ( non
empty )
set ) ) ;