:: BORSUK_4 semantic presentation
begin
registration
cluster
being_simple_closed_curve
->
non
trivial
being_simple_closed_curve
for ( ( ) ( )
Element
of
bool
the
carrier
of
(
TOP-REAL
2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
non
trivial
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) : ( ( ) (
functional
non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
end;
theorem
:: BORSUK_4:1
for
X
being ( ( non
empty
) ( non
empty
)
set
)
for
A
being ( ( non
empty
) ( non
empty
)
Subset
of ( ( ) ( non
empty
)
set
) ) st
A
: ( ( non
empty
) ( non
empty
)
Subset
of ( ( ) ( non
empty
)
set
) ) is
trivial
holds
ex
x
being ( ( ) ( )
Element
of
X
: ( ( non
empty
) ( non
empty
)
set
) ) st
A
: ( ( non
empty
) ( non
empty
)
Subset
of ( ( ) ( non
empty
)
set
) )
=
{
x
: ( ( ) ( )
Element
of
b
1
: ( ( non
empty
) ( non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
)
Element
of
bool
b
1
: ( ( non
empty
) ( non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BORSUK_4:2
for
X
being ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
for
p
being ( ( ) ( )
set
) ex
q
being ( ( ) ( )
Element
of
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ) st
q
: ( ( ) ( )
Element
of
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) )
<>
p
: ( ( ) ( )
set
) ;
theorem
:: BORSUK_4:3
for
T
being ( ( non
trivial
) ( non
empty
non
trivial
)
set
)
for
X
being ( ( non
trivial
) ( non
empty
non
trivial
)
Subset
of ( ( ) ( non
empty
)
set
) )
for
p
being ( ( ) ( )
set
) ex
q
being ( ( ) ( )
Element
of
T
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) ) st
(
q
: ( ( ) ( )
Element
of
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) )
in
X
: ( ( non
trivial
) ( non
empty
non
trivial
)
Subset
of ( ( ) ( non
empty
)
set
) ) &
q
: ( ( ) ( )
Element
of
b
1
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) )
<>
p
: ( ( ) ( )
set
) ) ;
theorem
:: BORSUK_4:4
for
f
,
g
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
for
a
being ( ( ) ( )
set
) st
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) is
one-to-one
&
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) is
one-to-one
&
(
dom
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
)
: ( ( ) ( )
set
)
/\
(
dom
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
)
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
=
{
a
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
)
set
) &
(
rng
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
)
: ( ( ) ( )
set
)
/\
(
rng
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
)
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
=
{
(
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
a
: ( ( ) ( )
set
)
)
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
)
set
) holds
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
+*
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) : ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
set
) is
one-to-one
;
theorem
:: BORSUK_4:5
for
f
,
g
being ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
for
a
being ( ( ) ( )
set
) st
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) is
one-to-one
&
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
) is
one-to-one
&
(
dom
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
)
: ( ( ) ( )
set
)
/\
(
dom
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
)
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
=
{
a
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
)
set
) &
(
rng
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
)
: ( ( ) ( )
set
)
/\
(
rng
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
)
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
=
{
(
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
a
: ( ( ) ( )
set
)
)
: ( ( ) ( )
set
)
}
: ( ( ) ( non
empty
trivial
)
set
) &
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
a
: ( ( ) ( )
set
) : ( ( ) ( )
set
)
=
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
.
a
: ( ( ) ( )
set
) : ( ( ) ( )
set
) holds
(
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
+*
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
)
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
set
)
"
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
set
)
=
(
f
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
"
)
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
set
)
+*
(
g
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
Function
)
"
)
: ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
set
) : ( (
Relation-like
Function-like
) (
Relation-like
Function-like
)
set
) ;
theorem
:: BORSUK_4:6
for
n
being ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
for
A
being ( ( ) ( )
Subset
of )
for
p
,
q
being ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) st
A
: ( ( ) ( )
Subset
of )
is_an_arc_of
p
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) ,
q
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) holds
not
A
: ( ( ) ( )
Subset
of )
\
{
p
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
closed
compact
bounded
)
Element
of
bool
the
carrier
of
(
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) ( )
Element
of
bool
the
carrier
of
(
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) is
empty
;
theorem
:: BORSUK_4:7
for
s1
,
s3
,
s4
,
l
being ( (
real
) (
V72
()
real
ext-real
)
number
) st
s1
: ( (
real
) (
V72
()
real
ext-real
)
number
)
<=
s3
: ( (
real
) (
V72
()
real
ext-real
)
number
) &
s1
: ( (
real
) (
V72
()
real
ext-real
)
number
)
<
s4
: ( (
real
) (
V72
()
real
ext-real
)
number
) &
0
: ( ( ) (
empty
trivial
natural
V72
()
real
ext-real
non
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
interval
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
<=
l
: ( (
real
) (
V72
()
real
ext-real
)
number
) &
l
: ( (
real
) (
V72
()
real
ext-real
)
number
)
<=
1 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) holds
s1
: ( (
real
) (
V72
()
real
ext-real
)
number
)
<=
(
(
1 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
-
l
: ( (
real
) (
V72
()
real
ext-real
)
number
)
)
: ( ( ) (
V72
()
real
ext-real
)
set
)
*
s3
: ( (
real
) (
V72
()
real
ext-real
)
number
)
)
: ( ( ) (
V72
()
real
ext-real
)
set
)
+
(
l
: ( (
real
) (
V72
()
real
ext-real
)
number
)
*
s4
: ( (
real
) (
V72
()
real
ext-real
)
number
)
)
: ( ( ) (
V72
()
real
ext-real
)
set
) : ( ( ) (
V72
()
real
ext-real
)
set
) ;
theorem
:: BORSUK_4:8
for
A
being ( ( ) (
V143
()
V144
()
V145
() )
Subset
of )
for
a
,
b
being ( (
real
) (
V72
()
real
ext-real
)
number
) st
a
: ( (
real
) (
V72
()
real
ext-real
)
number
)
<
b
: ( (
real
) (
V72
()
real
ext-real
)
number
) &
A
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of )
=
].
a
: ( (
real
) (
V72
()
real
ext-real
)
number
) ,
b
: ( (
real
) (
V72
()
real
ext-real
)
number
)
.[
: ( ( ) (
V143
()
V144
()
V145
()
open
non
left_end
non
right_end
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) holds
[.
a
: ( (
real
) (
V72
()
real
ext-real
)
number
) ,
b
: ( (
real
) (
V72
()
real
ext-real
)
number
)
.]
: ( ( ) (
V143
()
V144
()
V145
()
closed
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) )
c=
the
carrier
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) : ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ;
theorem
:: BORSUK_4:9
for
A
being ( ( ) (
V143
()
V144
()
V145
() )
Subset
of )
for
a
,
b
being ( (
real
) (
V72
()
real
ext-real
)
number
) st
a
: ( (
real
) (
V72
()
real
ext-real
)
number
)
<
b
: ( (
real
) (
V72
()
real
ext-real
)
number
) &
A
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of )
=
].
a
: ( (
real
) (
V72
()
real
ext-real
)
number
) ,
b
: ( (
real
) (
V72
()
real
ext-real
)
number
)
.]
: ( ( ) (
V143
()
V144
()
V145
() non
left_end
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) holds
[.
a
: ( (
real
) (
V72
()
real
ext-real
)
number
) ,
b
: ( (
real
) (
V72
()
real
ext-real
)
number
)
.]
: ( ( ) (
V143
()
V144
()
V145
()
closed
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) )
c=
the
carrier
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) : ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ;
theorem
:: BORSUK_4:10
for
A
being ( ( ) (
V143
()
V144
()
V145
() )
Subset
of )
for
a
,
b
being ( (
real
) (
V72
()
real
ext-real
)
number
) st
a
: ( (
real
) (
V72
()
real
ext-real
)
number
)
<
b
: ( (
real
) (
V72
()
real
ext-real
)
number
) &
A
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of )
=
[.
a
: ( (
real
) (
V72
()
real
ext-real
)
number
) ,
b
: ( (
real
) (
V72
()
real
ext-real
)
number
)
.[
: ( ( ) (
V143
()
V144
()
V145
() non
right_end
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) holds
[.
a
: ( (
real
) (
V72
()
real
ext-real
)
number
) ,
b
: ( (
real
) (
V72
()
real
ext-real
)
number
)
.]
: ( ( ) (
V143
()
V144
()
V145
()
closed
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) )
c=
the
carrier
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) : ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ;
theorem
:: BORSUK_4:11
for
a
,
b
being ( (
real
) (
V72
()
real
ext-real
)
number
) st
a
: ( (
real
) (
V72
()
real
ext-real
)
number
)
<>
b
: ( (
real
) (
V72
()
real
ext-real
)
number
) holds
Cl
].
a
: ( (
real
) (
V72
()
real
ext-real
)
number
) ,
b
: ( (
real
) (
V72
()
real
ext-real
)
number
)
.]
: ( ( ) (
V143
()
V144
()
V145
() non
left_end
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
V143
()
V144
()
V145
() )
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) )
=
[.
a
: ( (
real
) (
V72
()
real
ext-real
)
number
) ,
b
: ( (
real
) (
V72
()
real
ext-real
)
number
)
.]
: ( ( ) (
V143
()
V144
()
V145
()
closed
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BORSUK_4:12
for
a
,
b
being ( (
real
) (
V72
()
real
ext-real
)
number
) st
a
: ( (
real
) (
V72
()
real
ext-real
)
number
)
<>
b
: ( (
real
) (
V72
()
real
ext-real
)
number
) holds
Cl
[.
a
: ( (
real
) (
V72
()
real
ext-real
)
number
) ,
b
: ( (
real
) (
V72
()
real
ext-real
)
number
)
.[
: ( ( ) (
V143
()
V144
()
V145
() non
right_end
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( ( ) (
V143
()
V144
()
V145
() )
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) )
=
[.
a
: ( (
real
) (
V72
()
real
ext-real
)
number
) ,
b
: ( (
real
) (
V72
()
real
ext-real
)
number
)
.]
: ( ( ) (
V143
()
V144
()
V145
()
closed
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BORSUK_4:13
for
A
being ( ( ) (
V143
()
V144
()
V145
() )
Subset
of )
for
a
,
b
being ( (
real
) (
V72
()
real
ext-real
)
number
) st
a
: ( (
real
) (
V72
()
real
ext-real
)
number
)
<
b
: ( (
real
) (
V72
()
real
ext-real
)
number
) &
A
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of )
=
].
a
: ( (
real
) (
V72
()
real
ext-real
)
number
) ,
b
: ( (
real
) (
V72
()
real
ext-real
)
number
)
.[
: ( ( ) (
V143
()
V144
()
V145
()
open
non
left_end
non
right_end
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) holds
Cl
A
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ) : ( ( ) (
closed
V143
()
V144
()
V145
() )
Element
of
bool
the
carrier
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) : ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) : ( ( ) ( non
empty
)
set
) )
=
[.
a
: ( (
real
) (
V72
()
real
ext-real
)
number
) ,
b
: ( (
real
) (
V72
()
real
ext-real
)
number
)
.]
: ( ( ) (
V143
()
V144
()
V145
()
closed
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BORSUK_4:14
for
A
being ( ( ) (
V143
()
V144
()
V145
() )
Subset
of )
for
a
,
b
being ( (
real
) (
V72
()
real
ext-real
)
number
) st
a
: ( (
real
) (
V72
()
real
ext-real
)
number
)
<
b
: ( (
real
) (
V72
()
real
ext-real
)
number
) &
A
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of )
=
].
a
: ( (
real
) (
V72
()
real
ext-real
)
number
) ,
b
: ( (
real
) (
V72
()
real
ext-real
)
number
)
.]
: ( ( ) (
V143
()
V144
()
V145
() non
left_end
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) holds
Cl
A
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ) : ( ( ) (
closed
V143
()
V144
()
V145
() )
Element
of
bool
the
carrier
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) : ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) : ( ( ) ( non
empty
)
set
) )
=
[.
a
: ( (
real
) (
V72
()
real
ext-real
)
number
) ,
b
: ( (
real
) (
V72
()
real
ext-real
)
number
)
.]
: ( ( ) (
V143
()
V144
()
V145
()
closed
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BORSUK_4:15
for
A
being ( ( ) (
V143
()
V144
()
V145
() )
Subset
of )
for
a
,
b
being ( (
real
) (
V72
()
real
ext-real
)
number
) st
a
: ( (
real
) (
V72
()
real
ext-real
)
number
)
<
b
: ( (
real
) (
V72
()
real
ext-real
)
number
) &
A
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of )
=
[.
a
: ( (
real
) (
V72
()
real
ext-real
)
number
) ,
b
: ( (
real
) (
V72
()
real
ext-real
)
number
)
.[
: ( ( ) (
V143
()
V144
()
V145
() non
right_end
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) holds
Cl
A
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ) : ( ( ) (
closed
V143
()
V144
()
V145
() )
Element
of
bool
the
carrier
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) : ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) : ( ( ) ( non
empty
)
set
) )
=
[.
a
: ( (
real
) (
V72
()
real
ext-real
)
number
) ,
b
: ( (
real
) (
V72
()
real
ext-real
)
number
)
.]
: ( ( ) (
V143
()
V144
()
V145
()
closed
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BORSUK_4:16
for
A
being ( ( ) (
V143
()
V144
()
V145
() )
Subset
of )
for
a
,
b
being ( (
real
) (
V72
()
real
ext-real
)
number
) st
a
: ( (
real
) (
V72
()
real
ext-real
)
number
)
<=
b
: ( (
real
) (
V72
()
real
ext-real
)
number
) &
A
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of )
=
[.
a
: ( (
real
) (
V72
()
real
ext-real
)
number
) ,
b
: ( (
real
) (
V72
()
real
ext-real
)
number
)
.]
: ( ( ) (
V143
()
V144
()
V145
()
closed
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) holds
(
0
: ( ( ) (
empty
trivial
natural
V72
()
real
ext-real
non
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
interval
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
<=
a
: ( (
real
) (
V72
()
real
ext-real
)
number
) &
b
: ( (
real
) (
V72
()
real
ext-real
)
number
)
<=
1 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) ) ;
theorem
:: BORSUK_4:17
for
A
,
B
being ( ( ) (
V143
()
V144
()
V145
() )
Subset
of )
for
a
,
b
,
c
being ( (
real
) (
V72
()
real
ext-real
)
number
) st
a
: ( (
real
) (
V72
()
real
ext-real
)
number
)
<
b
: ( (
real
) (
V72
()
real
ext-real
)
number
) &
b
: ( (
real
) (
V72
()
real
ext-real
)
number
)
<
c
: ( (
real
) (
V72
()
real
ext-real
)
number
) &
A
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of )
=
[.
a
: ( (
real
) (
V72
()
real
ext-real
)
number
) ,
b
: ( (
real
) (
V72
()
real
ext-real
)
number
)
.[
: ( ( ) (
V143
()
V144
()
V145
() non
right_end
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) &
B
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of )
=
].
b
: ( (
real
) (
V72
()
real
ext-real
)
number
) ,
c
: ( (
real
) (
V72
()
real
ext-real
)
number
)
.]
: ( ( ) (
V143
()
V144
()
V145
() non
left_end
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) holds
A
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ) ,
B
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of )
are_separated
;
theorem
:: BORSUK_4:18
for
p1
,
p2
being ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) holds
[.
p1
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) ,
p2
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) )
.]
: ( ( ) (
V143
()
V144
()
V145
()
closed
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) is ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ) ;
theorem
:: BORSUK_4:19
for
a
,
b
being ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) holds
].
a
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) ,
b
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) )
.[
: ( ( ) (
V143
()
V144
()
V145
()
open
non
left_end
non
right_end
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) is ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ) ;
begin
theorem
:: BORSUK_4:20
for
p
being ( (
real
) (
V72
()
real
ext-real
)
number
) holds
{
p
: ( (
real
) (
V72
()
real
ext-real
)
number
)
}
: ( ( ) ( non
empty
trivial
V143
()
V144
()
V145
() )
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) is ( ( non
empty
closed_interval
) ( non
empty
V143
()
V144
()
V145
()
closed_interval
interval
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BORSUK_4:21
for
A
being ( ( non
empty
connected
) ( non
empty
connected
V143
()
V144
()
V145
() )
Subset
of )
for
a
,
b
,
c
being ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) st
a
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) )
<=
b
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) &
b
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) )
<=
c
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) &
a
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) )
in
A
: ( ( non
empty
connected
) ( non
empty
connected
V143
()
V144
()
V145
() )
Subset
of ) &
c
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) )
in
A
: ( ( non
empty
connected
) ( non
empty
connected
V143
()
V144
()
V145
() )
Subset
of ) holds
b
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) )
in
A
: ( ( non
empty
connected
) ( non
empty
connected
V143
()
V144
()
V145
() )
Subset
of ) ;
theorem
:: BORSUK_4:22
for
A
being ( ( non
empty
connected
) ( non
empty
connected
V143
()
V144
()
V145
() )
Subset
of )
for
a
,
b
being ( (
real
) (
V72
()
real
ext-real
)
number
) st
a
: ( (
real
) (
V72
()
real
ext-real
)
number
)
in
A
: ( ( non
empty
connected
) ( non
empty
connected
V143
()
V144
()
V145
() )
Subset
of ) &
b
: ( (
real
) (
V72
()
real
ext-real
)
number
)
in
A
: ( ( non
empty
connected
) ( non
empty
connected
V143
()
V144
()
V145
() )
Subset
of ) holds
[.
a
: ( (
real
) (
V72
()
real
ext-real
)
number
) ,
b
: ( (
real
) (
V72
()
real
ext-real
)
number
)
.]
: ( ( ) (
V143
()
V144
()
V145
()
closed
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) )
c=
A
: ( ( non
empty
connected
) ( non
empty
connected
V143
()
V144
()
V145
() )
Subset
of ) ;
theorem
:: BORSUK_4:23
for
a
,
b
being ( (
real
) (
V72
()
real
ext-real
)
number
)
for
A
being ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ) st
A
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of )
=
[.
a
: ( (
real
) (
V72
()
real
ext-real
)
number
) ,
b
: ( (
real
) (
V72
()
real
ext-real
)
number
)
.]
: ( ( ) (
V143
()
V144
()
V145
()
closed
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) holds
A
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ) is
closed
;
theorem
:: BORSUK_4:24
for
p1
,
p2
being ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) st
p1
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) )
<=
p2
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) holds
[.
p1
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) ,
p2
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) )
.]
: ( ( ) (
V143
()
V144
()
V145
()
closed
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) is ( ( non
empty
connected
compact
) ( non
empty
closed
connected
compact
V143
()
V144
()
V145
() )
Subset
of ) ;
theorem
:: BORSUK_4:25
for
X
being ( ( ) (
V143
()
V144
()
V145
() )
Subset
of )
for
X9
being ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ( ( ) ( non
empty
)
set
) ) st
X9
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ( ( ) ( non
empty
)
set
) )
=
X
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ) holds
(
X9
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ( ( ) ( non
empty
)
set
) ) is
bounded_above
&
X9
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ( ( ) ( non
empty
)
set
) ) is
bounded_below
) ;
theorem
:: BORSUK_4:26
for
X
being ( ( ) (
V143
()
V144
()
V145
() )
Subset
of )
for
X9
being ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ( ( ) ( non
empty
)
set
) )
for
x
being ( (
real
) (
V72
()
real
ext-real
)
number
) st
x
: ( (
real
) (
V72
()
real
ext-real
)
number
)
in
X9
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ( ( ) ( non
empty
)
set
) ) &
X9
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ( ( ) ( non
empty
)
set
) )
=
X
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ) holds
(
lower_bound
X9
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
V72
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) )
<=
x
: ( (
real
) (
V72
()
real
ext-real
)
number
) &
x
: ( (
real
) (
V72
()
real
ext-real
)
number
)
<=
upper_bound
X9
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
V72
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) ) ) ;
theorem
:: BORSUK_4:27
for
A
being ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ( ( ) ( non
empty
)
set
) )
for
B
being ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ) st
A
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ( ( ) ( non
empty
)
set
) )
=
B
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ) holds
(
A
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ( ( ) ( non
empty
)
set
) ) is
closed
iff
B
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ) is
closed
) ;
theorem
:: BORSUK_4:28
for
C
being ( ( non
empty
closed_interval
) ( non
empty
V143
()
V144
()
V145
()
closed_interval
interval
)
Subset
of ( ( ) ( non
empty
)
set
) ) holds
lower_bound
C
: ( ( non
empty
closed_interval
) ( non
empty
V143
()
V144
()
V145
()
closed_interval
interval
)
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
V72
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) )
<=
upper_bound
C
: ( ( non
empty
closed_interval
) ( non
empty
V143
()
V144
()
V145
()
closed_interval
interval
)
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
V72
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) ) ;
theorem
:: BORSUK_4:29
for
C
being ( ( non
empty
connected
compact
) ( non
empty
closed
connected
compact
V143
()
V144
()
V145
() )
Subset
of )
for
C9
being ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ( ( ) ( non
empty
)
set
) ) st
C
: ( ( non
empty
connected
compact
) ( non
empty
closed
connected
compact
V143
()
V144
()
V145
() )
Subset
of )
=
C9
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ( ( ) ( non
empty
)
set
) ) &
[.
(
lower_bound
C9
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
V72
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) ) ,
(
upper_bound
C9
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
V72
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) )
.]
: ( ( ) (
V143
()
V144
()
V145
()
closed
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) )
c=
C9
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ( ( ) ( non
empty
)
set
) ) holds
[.
(
lower_bound
C9
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
V72
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) ) ,
(
upper_bound
C9
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ( ( ) ( non
empty
)
set
) )
)
: ( ( ) (
V72
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) )
.]
: ( ( ) (
V143
()
V144
()
V145
()
closed
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) )
=
C9
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BORSUK_4:30
for
C
being ( ( non
empty
connected
compact
) ( non
empty
closed
connected
compact
V143
()
V144
()
V145
() )
Subset
of ) holds
C
: ( ( non
empty
connected
compact
) ( non
empty
closed
connected
compact
V143
()
V144
()
V145
() )
Subset
of ) is ( ( non
empty
closed_interval
) ( non
empty
V143
()
V144
()
V145
()
closed_interval
interval
)
Subset
of ( ( ) ( non
empty
)
set
) ) ;
theorem
:: BORSUK_4:31
for
C
being ( ( non
empty
connected
compact
) ( non
empty
closed
connected
compact
V143
()
V144
()
V145
() )
Subset
of ) ex
p1
,
p2
being ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) st
(
p1
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) )
<=
p2
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) &
C
: ( ( non
empty
connected
compact
) ( non
empty
closed
connected
compact
V143
()
V144
()
V145
() )
Subset
of )
=
[.
p1
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) ,
p2
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) )
.]
: ( ( ) (
V143
()
V144
()
V145
()
closed
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) ;
begin
definition
func
I(01)
->
( (
strict
) (
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
SubSpace
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) )
means
:: BORSUK_4:def 1
the
carrier
of
it
: ( ( non
trivial
) ( non
empty
non
trivial
)
set
) : ( ( ) ( )
set
)
=
].
0
: ( ( ) (
empty
trivial
natural
V72
()
real
ext-real
non
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
interval
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) ,1 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
.[
: ( ( ) (
V143
()
V144
()
V145
()
open
non
left_end
non
right_end
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ;
end;
registration
cluster
I(01)
: ( (
strict
) (
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
SubSpace
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) )
->
non
empty
strict
;
end;
theorem
:: BORSUK_4:32
for
A
being ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ) st
A
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of )
=
the
carrier
of
I(01)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
SubSpace
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) ) : ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) holds
I(01)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
SubSpace
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) )
=
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) )
|
A
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ) : ( (
strict
) (
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
SubSpace
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) ) ;
theorem
:: BORSUK_4:33
the
carrier
of
I(01)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
SubSpace
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) ) : ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
)
=
the
carrier
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) : ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
)
\
{
0
: ( ( ) (
empty
trivial
natural
V72
()
real
ext-real
non
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
interval
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) ,1 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
}
: ( ( ) ( non
empty
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
set
) : ( ( ) (
V143
()
V144
()
V145
() )
Element
of
bool
the
carrier
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) : ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) : ( ( ) ( non
empty
)
set
) ) ;
registration
cluster
I(01)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
SubSpace
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) )
->
strict
open
;
end;
theorem
:: BORSUK_4:34
I(01)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
open
V197
() )
SubSpace
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) ) is
open
;
theorem
:: BORSUK_4:35
for
r
being ( (
real
) (
V72
()
real
ext-real
)
number
) holds
(
r
: ( (
real
) (
V72
()
real
ext-real
)
number
)
in
the
carrier
of
I(01)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
open
V197
() )
SubSpace
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) ) : ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) iff (
0
: ( ( ) (
empty
trivial
natural
V72
()
real
ext-real
non
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
interval
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
<
r
: ( (
real
) (
V72
()
real
ext-real
)
number
) &
r
: ( (
real
) (
V72
()
real
ext-real
)
number
)
<
1 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) ) ) ;
theorem
:: BORSUK_4:36
for
a
,
b
being ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) st
a
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) )
<
b
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) &
b
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) )
<>
1 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) holds
].
a
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) ,
b
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) )
.]
: ( ( ) (
V143
()
V144
()
V145
() non
left_end
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) is ( ( non
empty
) ( non
empty
V143
()
V144
()
V145
() )
Subset
of ) ;
theorem
:: BORSUK_4:37
for
a
,
b
being ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) st
a
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) )
<
b
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) &
a
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) )
<>
0
: ( ( ) (
empty
trivial
natural
V72
()
real
ext-real
non
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
interval
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) holds
[.
a
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) ,
b
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) )
.[
: ( ( ) (
V143
()
V144
()
V145
() non
right_end
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) is ( ( non
empty
) ( non
empty
V143
()
V144
()
V145
() )
Subset
of ) ;
theorem
:: BORSUK_4:38
for
D
being ( (
being_simple_closed_curve
) ( non
empty
non
trivial
closed
connected
compact
bounded
being_simple_closed_curve
)
Simple_closed_curve
) holds
(
TOP-REAL
2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
non
trivial
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
)
|
R^2-unit_square
: ( ( ) ( non
empty
non
trivial
closed
connected
compact
bounded
being_simple_closed_curve
)
Element
of
bool
the
carrier
of
(
TOP-REAL
2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
non
trivial
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) : ( ( ) (
functional
non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
)
SubSpace
of
TOP-REAL
2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( (
strict
) ( non
empty
non
trivial
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) ) ,
(
TOP-REAL
2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
non
trivial
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
)
|
D
: ( (
being_simple_closed_curve
) ( non
empty
non
trivial
closed
connected
compact
bounded
being_simple_closed_curve
)
Simple_closed_curve
) : ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
)
SubSpace
of
TOP-REAL
2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( (
strict
) ( non
empty
non
trivial
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) )
are_homeomorphic
;
theorem
:: BORSUK_4:39
for
n
being ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
for
D
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
p1
,
p2
being ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) st
D
: ( ( non
empty
) ( non
empty
)
Subset
of )
is_an_arc_of
p1
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) ,
p2
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) holds
I(01)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
open
V197
() )
SubSpace
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) ) ,
(
TOP-REAL
n
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
)
|
(
D
: ( ( non
empty
) ( non
empty
)
Subset
of )
\
{
p1
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) ,
p2
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
}
: ( ( ) ( non
empty
)
Element
of
bool
the
carrier
of
(
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
(
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( (
strict
) (
strict
TopSpace-like
T_0
T_1
T_2
)
SubSpace
of
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) )
are_homeomorphic
;
theorem
:: BORSUK_4:40
for
n
being ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
for
D
being ( ( ) ( )
Subset
of )
for
p1
,
p2
being ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) st
D
: ( ( ) ( )
Subset
of )
is_an_arc_of
p1
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) ,
p2
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) holds
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) ,
(
TOP-REAL
n
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
)
|
D
: ( ( ) ( )
Subset
of ) : ( (
strict
) (
strict
TopSpace-like
T_0
T_1
T_2
)
SubSpace
of
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) )
are_homeomorphic
;
theorem
:: BORSUK_4:41
for
n
being ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
for
p1
,
p2
being ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) st
p1
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
<>
p2
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) holds
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) ,
(
TOP-REAL
n
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
)
|
(
LSeg
(
p1
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) ,
p2
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) )
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
(
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( (
strict
) (
strict
TopSpace-like
T_0
T_1
T_2
)
SubSpace
of
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) )
are_homeomorphic
;
theorem
:: BORSUK_4:42
for
E
being ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ) st ex
p1
,
p2
being ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) st
(
p1
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) )
<
p2
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) &
E
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of )
=
[.
p1
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) ,
p2
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) )
.]
: ( ( ) (
V143
()
V144
()
V145
()
closed
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) holds
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) ,
I(01)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
open
V197
() )
SubSpace
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) )
|
E
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ) : ( (
strict
) (
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
SubSpace
of
I(01)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
open
V197
() )
SubSpace
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) ) )
are_homeomorphic
;
theorem
:: BORSUK_4:43
for
n
being ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
for
A
being ( ( ) ( )
Subset
of )
for
p
,
q
being ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
for
a
,
b
being ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) st
A
: ( ( ) ( )
Subset
of )
is_an_arc_of
p
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) ,
q
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) &
a
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) )
<
b
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) holds
ex
E
being ( ( non
empty
) ( non
empty
V143
()
V144
()
V145
() )
Subset
of ) 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
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) )
|
b
7
: ( ( non
empty
) ( non
empty
V143
()
V144
()
V145
() )
Subset
of )
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
SubSpace
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) ) : ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
)
-defined
the
carrier
of
(
(
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
)
|
b
2
: ( ( ) ( )
Subset
of )
)
: ( (
strict
) (
strict
TopSpace-like
T_0
T_1
T_2
)
SubSpace
of
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) ) : ( ( ) ( )
set
)
-valued
Function-like
quasi_total
)
Function
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) , ( ( ) ( )
set
) ) st
(
E
: ( ( non
empty
) ( non
empty
V143
()
V144
()
V145
() )
Subset
of )
=
[.
a
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) ,
b
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) )
.]
: ( ( ) (
V143
()
V144
()
V145
()
closed
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( 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
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) )
|
b
7
: ( ( non
empty
) ( non
empty
V143
()
V144
()
V145
() )
Subset
of )
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
SubSpace
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) ) : ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
)
-defined
the
carrier
of
(
(
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
)
|
b
2
: ( ( ) ( )
Subset
of )
)
: ( (
strict
) (
strict
TopSpace-like
T_0
T_1
T_2
)
SubSpace
of
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) ) : ( ( ) ( )
set
)
-valued
Function-like
quasi_total
)
Function
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) , ( ( ) ( )
set
) ) is
being_homeomorphism
&
f
: ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
(
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) )
|
b
7
: ( ( non
empty
) ( non
empty
V143
()
V144
()
V145
() )
Subset
of )
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
SubSpace
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) ) : ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
)
-defined
the
carrier
of
(
(
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
)
|
b
2
: ( ( ) ( )
Subset
of )
)
: ( (
strict
) (
strict
TopSpace-like
T_0
T_1
T_2
)
SubSpace
of
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) ) : ( ( ) ( )
set
)
-valued
Function-like
quasi_total
)
Function
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) , ( ( ) ( )
set
) )
.
a
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) : ( ( ) ( )
set
)
=
p
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
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
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) )
|
b
7
: ( ( non
empty
) ( non
empty
V143
()
V144
()
V145
() )
Subset
of )
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
SubSpace
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) ) : ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
)
-defined
the
carrier
of
(
(
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
)
|
b
2
: ( ( ) ( )
Subset
of )
)
: ( (
strict
) (
strict
TopSpace-like
T_0
T_1
T_2
)
SubSpace
of
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) ) : ( ( ) ( )
set
)
-valued
Function-like
quasi_total
)
Function
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) , ( ( ) ( )
set
) )
.
b
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) : ( ( ) ( )
set
)
=
q
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) ) ;
theorem
:: BORSUK_4:44
for
A
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
B
being ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
)
for
f
being ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
total
quasi_total
)
Function
of ( ( ) ( )
set
) , ( ( ) ( non
empty
)
set
) )
for
C
being ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
for
X
being ( ( ) ( )
Subset
of ) st
f
: ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
total
quasi_total
)
Function
of ( ( ) ( )
set
) , ( ( ) ( non
empty
)
set
) ) is
continuous
&
C
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) is ( ( ) (
TopSpace-like
)
SubSpace
of
B
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) ) holds
for
h
being ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
(
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
|
b
5
: ( ( ) ( )
Subset
of )
)
: ( (
strict
) (
strict
TopSpace-like
)
SubSpace
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
4
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
)
-valued
Function-like
quasi_total
)
Function
of ( ( ) ( )
set
) , ( ( ) ( )
set
) ) st
h
: ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
(
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
|
b
5
: ( ( ) ( )
Subset
of )
)
: ( (
strict
) (
strict
TopSpace-like
)
SubSpace
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
4
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
)
-valued
Function-like
quasi_total
)
Function
of ( ( ) ( )
set
) , ( ( ) ( )
set
) )
=
f
: ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
total
quasi_total
)
Function
of ( ( ) ( )
set
) , ( ( ) ( non
empty
)
set
) )
|
X
: ( ( ) ( )
Subset
of ) : ( (
Function-like
) (
Relation-like
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
)
Element
of
bool
[:
the
carrier
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
) , the
carrier
of
b
2
: ( ( non
empty
TopSpace-like
) ( non
empty
TopSpace-like
)
TopSpace
) : ( ( ) ( non
empty
)
set
)
:]
: ( ( ) ( )
set
) : ( ( ) ( non
empty
)
set
) ) holds
h
: ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
(
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
)
|
b
5
: ( ( ) ( )
Subset
of )
)
: ( (
strict
) (
strict
TopSpace-like
)
SubSpace
of
b
1
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) ) : ( ( ) ( )
set
)
-defined
the
carrier
of
b
4
: ( (
TopSpace-like
) (
TopSpace-like
)
TopSpace
) : ( ( ) ( )
set
)
-valued
Function-like
quasi_total
)
Function
of ( ( ) ( )
set
) , ( ( ) ( )
set
) ) is
continuous
;
theorem
:: BORSUK_4:45
for
X
being ( ( ) (
V143
()
V144
()
V145
() )
Subset
of )
for
a
,
b
being ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) st
X
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of )
=
].
a
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) ,
b
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) )
.[
: ( ( ) (
V143
()
V144
()
V145
()
open
non
left_end
non
right_end
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) holds
X
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ) is
open
;
theorem
:: BORSUK_4:46
for
X
being ( ( ) (
V143
()
V144
()
V145
() )
Subset
of )
for
a
,
b
being ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) st
X
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of )
=
].
a
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) ,
b
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) )
.[
: ( ( ) (
V143
()
V144
()
V145
()
open
non
left_end
non
right_end
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) holds
X
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ) is
open
;
theorem
:: BORSUK_4:47
for
X
being ( ( ) (
V143
()
V144
()
V145
() )
Subset
of )
for
a
being ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) st
X
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of )
=
].
0
: ( ( ) (
empty
trivial
natural
V72
()
real
ext-real
non
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
interval
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) ,
a
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) )
.]
: ( ( ) (
V143
()
V144
()
V145
() non
left_end
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) holds
X
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ) is
closed
;
theorem
:: BORSUK_4:48
for
X
being ( ( ) (
V143
()
V144
()
V145
() )
Subset
of )
for
a
being ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) st
X
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of )
=
[.
a
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) ,1 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
.[
: ( ( ) (
V143
()
V144
()
V145
() non
right_end
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) holds
X
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ) is
closed
;
theorem
:: BORSUK_4:49
for
n
being ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
for
A
being ( ( ) ( )
Subset
of )
for
p
,
q
being ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
for
a
,
b
being ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) st
A
: ( ( ) ( )
Subset
of )
is_an_arc_of
p
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) ,
q
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) &
a
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) )
<
b
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) &
b
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) )
<>
1 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) holds
ex
E
being ( ( non
empty
) ( non
empty
V143
()
V144
()
V145
() )
Subset
of ) ex
f
being ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
(
I(01)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
open
V197
() )
SubSpace
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) )
|
b
7
: ( ( non
empty
) ( non
empty
V143
()
V144
()
V145
() )
Subset
of )
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
SubSpace
of
I(01)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
open
V197
() )
SubSpace
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) ) ) : ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
)
-defined
the
carrier
of
(
(
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
)
|
(
b
2
: ( ( ) ( )
Subset
of )
\
{
b
3
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
closed
compact
bounded
)
Element
of
bool
the
carrier
of
(
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
(
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( (
strict
) (
strict
TopSpace-like
T_0
T_1
T_2
)
SubSpace
of
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) ) : ( ( ) ( )
set
)
-valued
Function-like
quasi_total
)
Function
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) , ( ( ) ( )
set
) ) st
(
E
: ( ( non
empty
) ( non
empty
V143
()
V144
()
V145
() )
Subset
of )
=
].
a
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) ,
b
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) )
.]
: ( ( ) (
V143
()
V144
()
V145
() non
left_end
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) &
f
: ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
(
I(01)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
open
V197
() )
SubSpace
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) )
|
b
7
: ( ( non
empty
) ( non
empty
V143
()
V144
()
V145
() )
Subset
of )
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
SubSpace
of
I(01)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
open
V197
() )
SubSpace
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) ) ) : ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
)
-defined
the
carrier
of
(
(
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
)
|
(
b
2
: ( ( ) ( )
Subset
of )
\
{
b
3
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
closed
compact
bounded
)
Element
of
bool
the
carrier
of
(
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
(
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( (
strict
) (
strict
TopSpace-like
T_0
T_1
T_2
)
SubSpace
of
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) ) : ( ( ) ( )
set
)
-valued
Function-like
quasi_total
)
Function
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) , ( ( ) ( )
set
) ) is
being_homeomorphism
&
f
: ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
(
I(01)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
open
V197
() )
SubSpace
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) )
|
b
7
: ( ( non
empty
) ( non
empty
V143
()
V144
()
V145
() )
Subset
of )
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
SubSpace
of
I(01)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
open
V197
() )
SubSpace
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) ) ) : ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
)
-defined
the
carrier
of
(
(
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
)
|
(
b
2
: ( ( ) ( )
Subset
of )
\
{
b
3
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
closed
compact
bounded
)
Element
of
bool
the
carrier
of
(
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
(
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( (
strict
) (
strict
TopSpace-like
T_0
T_1
T_2
)
SubSpace
of
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) ) : ( ( ) ( )
set
)
-valued
Function-like
quasi_total
)
Function
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) , ( ( ) ( )
set
) )
.
b
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) : ( ( ) ( )
set
)
=
q
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) ) ;
theorem
:: BORSUK_4:50
for
n
being ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
for
A
being ( ( ) ( )
Subset
of )
for
p
,
q
being ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
for
a
,
b
being ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) st
A
: ( ( ) ( )
Subset
of )
is_an_arc_of
p
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) ,
q
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) &
a
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) )
<
b
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) &
a
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) )
<>
0
: ( ( ) (
empty
trivial
natural
V72
()
real
ext-real
non
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
interval
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) holds
ex
E
being ( ( non
empty
) ( non
empty
V143
()
V144
()
V145
() )
Subset
of ) ex
f
being ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
(
I(01)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
open
V197
() )
SubSpace
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) )
|
b
7
: ( ( non
empty
) ( non
empty
V143
()
V144
()
V145
() )
Subset
of )
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
SubSpace
of
I(01)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
open
V197
() )
SubSpace
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) ) ) : ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
)
-defined
the
carrier
of
(
(
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
)
|
(
b
2
: ( ( ) ( )
Subset
of )
\
{
b
4
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
closed
compact
bounded
)
Element
of
bool
the
carrier
of
(
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
(
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( (
strict
) (
strict
TopSpace-like
T_0
T_1
T_2
)
SubSpace
of
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) ) : ( ( ) ( )
set
)
-valued
Function-like
quasi_total
)
Function
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) , ( ( ) ( )
set
) ) st
(
E
: ( ( non
empty
) ( non
empty
V143
()
V144
()
V145
() )
Subset
of )
=
[.
a
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) ,
b
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) )
.[
: ( ( ) (
V143
()
V144
()
V145
() non
right_end
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) &
f
: ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
(
I(01)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
open
V197
() )
SubSpace
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) )
|
b
7
: ( ( non
empty
) ( non
empty
V143
()
V144
()
V145
() )
Subset
of )
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
SubSpace
of
I(01)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
open
V197
() )
SubSpace
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) ) ) : ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
)
-defined
the
carrier
of
(
(
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
)
|
(
b
2
: ( ( ) ( )
Subset
of )
\
{
b
4
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
closed
compact
bounded
)
Element
of
bool
the
carrier
of
(
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
(
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( (
strict
) (
strict
TopSpace-like
T_0
T_1
T_2
)
SubSpace
of
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) ) : ( ( ) ( )
set
)
-valued
Function-like
quasi_total
)
Function
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) , ( ( ) ( )
set
) ) is
being_homeomorphism
&
f
: ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
(
I(01)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
open
V197
() )
SubSpace
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) )
|
b
7
: ( ( non
empty
) ( non
empty
V143
()
V144
()
V145
() )
Subset
of )
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
SubSpace
of
I(01)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
open
V197
() )
SubSpace
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) ) ) : ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
)
-defined
the
carrier
of
(
(
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
)
|
(
b
2
: ( ( ) ( )
Subset
of )
\
{
b
4
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
closed
compact
bounded
)
Element
of
bool
the
carrier
of
(
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
(
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( (
strict
) (
strict
TopSpace-like
T_0
T_1
T_2
)
SubSpace
of
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) ) : ( ( ) ( )
set
)
-valued
Function-like
quasi_total
)
Function
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) , ( ( ) ( )
set
) )
.
a
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) : ( ( ) ( )
set
)
=
p
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) ) ;
theorem
:: BORSUK_4:51
for
n
being ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
for
A
,
B
being ( ( ) ( )
Subset
of )
for
p
,
q
being ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) st
A
: ( ( ) ( )
Subset
of )
is_an_arc_of
p
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) ,
q
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) &
B
: ( ( ) ( )
Subset
of )
is_an_arc_of
q
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) ,
p
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) &
A
: ( ( ) ( )
Subset
of )
/\
B
: ( ( ) ( )
Subset
of ) : ( ( ) ( )
Element
of
bool
the
carrier
of
(
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
=
{
p
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) ,
q
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
}
: ( ( ) ( non
empty
)
Element
of
bool
the
carrier
of
(
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) &
p
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
<>
q
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) holds
I(01)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
open
V197
() )
SubSpace
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) ) ,
(
TOP-REAL
n
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
)
|
(
(
A
: ( ( ) ( )
Subset
of )
\
{
p
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
closed
compact
bounded
)
Element
of
bool
the
carrier
of
(
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
(
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
\/
(
B
: ( ( ) ( )
Subset
of )
\
{
p
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
}
: ( ( ) ( non
empty
trivial
closed
compact
bounded
)
Element
of
bool
the
carrier
of
(
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
(
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
(
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( (
strict
) (
strict
TopSpace-like
T_0
T_1
T_2
)
SubSpace
of
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) )
are_homeomorphic
;
theorem
:: BORSUK_4:52
for
D
being ( (
being_simple_closed_curve
) ( non
empty
non
trivial
closed
connected
compact
bounded
being_simple_closed_curve
)
Simple_closed_curve
)
for
p
being ( ( ) (
V35
(2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
non
trivial
)
set
) ) st
p
: ( ( ) (
V35
(2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
non
trivial
)
set
) )
in
D
: ( (
being_simple_closed_curve
) ( non
empty
non
trivial
closed
connected
compact
bounded
being_simple_closed_curve
)
Simple_closed_curve
) holds
(
TOP-REAL
2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
non
trivial
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
)
|
(
D
: ( (
being_simple_closed_curve
) ( non
empty
non
trivial
closed
connected
compact
bounded
being_simple_closed_curve
)
Simple_closed_curve
)
\
{
p
: ( ( ) (
V35
(2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
non
trivial
)
set
) )
}
: ( ( ) ( non
empty
trivial
closed
compact
bounded
)
Element
of
bool
the
carrier
of
(
TOP-REAL
2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
non
trivial
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) : ( ( ) (
functional
non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
(
TOP-REAL
2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
non
trivial
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) : ( ( ) (
functional
non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( (
strict
) (
strict
TopSpace-like
T_0
T_1
T_2
)
SubSpace
of
TOP-REAL
2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( (
strict
) ( non
empty
non
trivial
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) ) ,
I(01)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
open
V197
() )
SubSpace
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) )
are_homeomorphic
;
theorem
:: BORSUK_4:53
for
D
being ( (
being_simple_closed_curve
) ( non
empty
non
trivial
closed
connected
compact
bounded
being_simple_closed_curve
)
Simple_closed_curve
)
for
p
,
q
being ( ( ) (
V35
(2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
non
trivial
)
set
) ) st
p
: ( ( ) (
V35
(2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
non
trivial
)
set
) )
in
D
: ( (
being_simple_closed_curve
) ( non
empty
non
trivial
closed
connected
compact
bounded
being_simple_closed_curve
)
Simple_closed_curve
) &
q
: ( ( ) (
V35
(2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
non
trivial
)
set
) )
in
D
: ( (
being_simple_closed_curve
) ( non
empty
non
trivial
closed
connected
compact
bounded
being_simple_closed_curve
)
Simple_closed_curve
) holds
(
TOP-REAL
2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
non
trivial
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
)
|
(
D
: ( (
being_simple_closed_curve
) ( non
empty
non
trivial
closed
connected
compact
bounded
being_simple_closed_curve
)
Simple_closed_curve
)
\
{
p
: ( ( ) (
V35
(2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
non
trivial
)
set
) )
}
: ( ( ) ( non
empty
trivial
closed
compact
bounded
)
Element
of
bool
the
carrier
of
(
TOP-REAL
2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
non
trivial
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) : ( ( ) (
functional
non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
(
TOP-REAL
2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
non
trivial
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) : ( ( ) (
functional
non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( (
strict
) (
strict
TopSpace-like
T_0
T_1
T_2
)
SubSpace
of
TOP-REAL
2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( (
strict
) ( non
empty
non
trivial
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) ) ,
(
TOP-REAL
2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
non
trivial
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
)
|
(
D
: ( (
being_simple_closed_curve
) ( non
empty
non
trivial
closed
connected
compact
bounded
being_simple_closed_curve
)
Simple_closed_curve
)
\
{
q
: ( ( ) (
V35
(2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
non
trivial
)
set
) )
}
: ( ( ) ( non
empty
trivial
closed
compact
bounded
)
Element
of
bool
the
carrier
of
(
TOP-REAL
2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
non
trivial
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) : ( ( ) (
functional
non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) )
)
: ( ( ) ( )
Element
of
bool
the
carrier
of
(
TOP-REAL
2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
non
trivial
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) : ( ( ) (
functional
non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) : ( (
strict
) (
strict
TopSpace-like
T_0
T_1
T_2
)
SubSpace
of
TOP-REAL
2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( (
strict
) ( non
empty
non
trivial
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) )
are_homeomorphic
;
theorem
:: BORSUK_4:54
for
n
being ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
for
C
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
E
being ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ) st ex
p1
,
p2
being ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) st
(
p1
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
<
p2
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) &
E
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of )
=
[.
p1
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) ,
p2
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
.]
: ( ( ) (
V143
()
V144
()
V145
() )
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) &
I(01)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
open
V197
() )
SubSpace
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) )
|
E
: ( ( ) (
V143
()
V144
()
V145
() )
Subset
of ) : ( (
strict
) (
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
SubSpace
of
I(01)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
open
V197
() )
SubSpace
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) ) ) ,
(
TOP-REAL
n
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
)
|
C
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
)
SubSpace
of
TOP-REAL
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) )
are_homeomorphic
holds
ex
s1
,
s2
being ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) st
C
: ( ( non
empty
) ( non
empty
)
Subset
of )
is_an_arc_of
s1
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) ,
s2
: ( ( ) (
V35
(
b
1
: ( ( ) (
natural
V72
()
real
ext-real
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) ;
theorem
:: BORSUK_4:55
for
Dp
being ( ( non
empty
) ( non
empty
)
Subset
of )
for
f
being ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
(
(
TOP-REAL
2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
non
trivial
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
)
|
b
1
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
)
SubSpace
of
TOP-REAL
2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( (
strict
) ( non
empty
non
trivial
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) ) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
I(01)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
open
V197
() )
SubSpace
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) ) : ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
)
-valued
Function-like
non
empty
total
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) )
for
C
being ( ( non
empty
) ( non
empty
)
Subset
of ) st
f
: ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
(
(
TOP-REAL
2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
non
trivial
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
)
|
b
1
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
)
SubSpace
of
TOP-REAL
2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( (
strict
) ( non
empty
non
trivial
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) ) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
I(01)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
open
V197
() )
SubSpace
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) ) : ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
)
-valued
Function-like
non
empty
total
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) is
being_homeomorphism
&
C
: ( ( non
empty
) ( non
empty
)
Subset
of )
c=
Dp
: ( ( non
empty
) ( non
empty
)
Subset
of ) & ex
p1
,
p2
being ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) st
(
p1
: ( ( ) (
V35
(2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
non
trivial
)
set
) )
<
p2
: ( ( ) (
V35
(2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
non
trivial
)
set
) ) &
f
: ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
(
(
TOP-REAL
2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
non
trivial
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
)
|
b
1
: ( ( non
empty
) ( non
empty
)
Subset
of )
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
)
SubSpace
of
TOP-REAL
2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) : ( (
strict
) ( non
empty
non
trivial
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) ) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
I(01)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
open
V197
() )
SubSpace
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) ) : ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
)
-valued
Function-like
non
empty
total
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) )
.:
C
: ( ( non
empty
) ( non
empty
)
Subset
of ) : ( ( ) (
V143
()
V144
()
V145
() )
Element
of
bool
the
carrier
of
I(01)
: ( (
strict
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
open
V197
() )
SubSpace
of
I[01]
: ( ( ) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
compact
V197
() )
SubSpace
of
R^1
: ( (
TopSpace-like
) ( non
empty
strict
TopSpace-like
T_0
T_1
T_2
V197
() )
TopStruct
) ) ) : ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) : ( ( ) ( non
empty
)
set
) )
=
[.
p1
: ( ( ) (
V35
(2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
non
trivial
)
set
) ) ,
p2
: ( ( ) (
V35
(2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
non
trivial
)
set
) )
.]
: ( ( ) (
V143
()
V144
()
V145
() )
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) holds
ex
s1
,
s2
being ( ( ) (
V35
(2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
non
trivial
)
set
) ) st
C
: ( ( non
empty
) ( non
empty
)
Subset
of )
is_an_arc_of
s1
: ( ( ) (
V35
(2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
non
trivial
)
set
) ) ,
s2
: ( ( ) (
V35
(2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
non
trivial
)
set
) ) ;
theorem
:: BORSUK_4:56
for
D
being ( (
being_simple_closed_curve
) ( non
empty
non
trivial
closed
connected
compact
bounded
being_simple_closed_curve
)
Simple_closed_curve
)
for
C
being ( ( non
empty
connected
compact
) ( non
empty
closed
connected
compact
bounded
)
Subset
of ) holds
( not
C
: ( ( non
empty
connected
compact
) ( non
empty
closed
connected
compact
bounded
)
Subset
of )
c=
D
: ( (
being_simple_closed_curve
) ( non
empty
non
trivial
closed
connected
compact
bounded
being_simple_closed_curve
)
Simple_closed_curve
) or
C
: ( ( non
empty
connected
compact
) ( non
empty
closed
connected
compact
bounded
)
Subset
of )
=
D
: ( (
being_simple_closed_curve
) ( non
empty
non
trivial
closed
connected
compact
bounded
being_simple_closed_curve
)
Simple_closed_curve
) or ex
p1
,
p2
being ( ( ) (
V35
(2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
non
trivial
)
set
) ) st
C
: ( ( non
empty
connected
compact
) ( non
empty
closed
connected
compact
bounded
)
Subset
of )
is_an_arc_of
p1
: ( ( ) (
V35
(2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
non
trivial
)
set
) ) ,
p2
: ( ( ) (
V35
(2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
non
trivial
)
set
) ) or ex
p
being ( ( ) (
V35
(2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
non
trivial
)
set
) ) st
C
: ( ( non
empty
connected
compact
) ( non
empty
closed
connected
compact
bounded
)
Subset
of )
=
{
p
: ( ( ) (
V35
(2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
non
trivial
)
set
) )
}
: ( ( ) ( non
empty
trivial
closed
compact
bounded
)
Element
of
bool
the
carrier
of
(
TOP-REAL
2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
)
: ( (
strict
) ( non
empty
non
trivial
TopSpace-like
T_0
T_1
T_2
V109
()
V155
()
V156
()
V157
()
V158
()
V159
()
V160
()
V161
()
strict
add-continuous
Mult-continuous
)
RLTopStruct
) : ( ( ) (
functional
non
empty
non
trivial
)
set
) : ( ( ) ( non
empty
)
set
) ) ) ;
begin
theorem
:: BORSUK_4:57
for
C
being ( ( non
empty
compact
) ( non
empty
closed
compact
V143
()
V144
()
V145
() )
Subset
of ) st
C
: ( ( non
empty
compact
) ( non
empty
closed
compact
V143
()
V144
()
V145
() )
Subset
of )
c=
].
0
: ( ( ) (
empty
trivial
natural
V72
()
real
ext-real
non
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
interval
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) ,1 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
.[
: ( ( ) (
V143
()
V144
()
V145
()
open
non
left_end
non
right_end
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) holds
ex
D
being ( ( non
empty
closed_interval
) ( non
empty
V143
()
V144
()
V145
()
closed_interval
interval
)
Subset
of ( ( ) ( non
empty
)
set
) ) st
(
C
: ( ( non
empty
compact
) ( non
empty
closed
compact
V143
()
V144
()
V145
() )
Subset
of )
c=
D
: ( ( non
empty
closed_interval
) ( non
empty
V143
()
V144
()
V145
()
closed_interval
interval
)
Subset
of ( ( ) ( non
empty
)
set
) ) &
D
: ( ( non
empty
closed_interval
) ( non
empty
V143
()
V144
()
V145
()
closed_interval
interval
)
Subset
of ( ( ) ( non
empty
)
set
) )
c=
].
0
: ( ( ) (
empty
trivial
natural
V72
()
real
ext-real
non
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
interval
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) ,1 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
.[
: ( ( ) (
V143
()
V144
()
V145
()
open
non
left_end
non
right_end
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) &
lower_bound
C
: ( ( non
empty
compact
) ( non
empty
closed
compact
V143
()
V144
()
V145
() )
Subset
of ) : ( (
real
) (
V72
()
real
ext-real
)
set
)
=
lower_bound
D
: ( ( non
empty
closed_interval
) ( non
empty
V143
()
V144
()
V145
()
closed_interval
interval
)
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
V72
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) ) &
upper_bound
C
: ( ( non
empty
compact
) ( non
empty
closed
compact
V143
()
V144
()
V145
() )
Subset
of ) : ( (
real
) (
V72
()
real
ext-real
)
set
)
=
upper_bound
D
: ( ( non
empty
closed_interval
) ( non
empty
V143
()
V144
()
V145
()
closed_interval
interval
)
Subset
of ( ( ) ( non
empty
)
set
) ) : ( ( ) (
V72
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) ) ) ;
theorem
:: BORSUK_4:58
for
C
being ( ( non
empty
compact
) ( non
empty
closed
compact
V143
()
V144
()
V145
() )
Subset
of ) st
C
: ( ( non
empty
compact
) ( non
empty
closed
compact
V143
()
V144
()
V145
() )
Subset
of )
c=
].
0
: ( ( ) (
empty
trivial
natural
V72
()
real
ext-real
non
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
interval
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) ,1 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
.[
: ( ( ) (
V143
()
V144
()
V145
()
open
non
left_end
non
right_end
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) holds
ex
p1
,
p2
being ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) st
(
p1
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) )
<=
p2
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) &
C
: ( ( non
empty
compact
) ( non
empty
closed
compact
V143
()
V144
()
V145
() )
Subset
of )
c=
[.
p1
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) ,
p2
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) )
.]
: ( ( ) (
V143
()
V144
()
V145
()
closed
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) &
[.
p1
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) ) ,
p2
: ( ( ) (
V72
()
real
ext-real
)
Point
of ( ( ) ( non
empty
V143
()
V144
()
V145
() )
set
) )
.]
: ( ( ) (
V143
()
V144
()
V145
()
closed
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) )
c=
].
0
: ( ( ) (
empty
trivial
natural
V72
()
real
ext-real
non
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
interval
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) ,1 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) )
.[
: ( ( ) (
V143
()
V144
()
V145
()
open
non
left_end
non
right_end
interval
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) ;
theorem
:: BORSUK_4:59
for
D
being ( (
being_simple_closed_curve
) ( non
empty
non
trivial
closed
connected
compact
bounded
being_simple_closed_curve
)
Simple_closed_curve
)
for
C
being ( (
closed
) (
closed
)
Subset
of ) st
C
: ( (
closed
) (
closed
)
Subset
of )
c<
D
: ( (
being_simple_closed_curve
) ( non
empty
non
trivial
closed
connected
compact
bounded
being_simple_closed_curve
)
Simple_closed_curve
) holds
ex
p1
,
p2
being ( ( ) (
V35
(2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
non
trivial
)
set
) ) ex
B
being ( ( ) ( )
Subset
of ) st
(
B
: ( ( ) ( )
Subset
of )
is_an_arc_of
p1
: ( ( ) (
V35
(2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
non
trivial
)
set
) ) ,
p2
: ( ( ) (
V35
(2 : ( ( ) ( non
empty
natural
V72
()
real
ext-real
positive
non
negative
V80
()
V81
()
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
left_end
bounded_below
)
Element
of
NAT
: ( ( ) (
V143
()
V144
()
V145
()
V146
()
V147
()
V148
()
V149
()
bounded_below
)
Element
of
bool
REAL
: ( ( ) (
V143
()
V144
()
V145
()
V149
() non
bounded_below
non
bounded_above
interval
)
set
) : ( ( ) ( non
empty
)
set
) ) ) )
V77
()
V135
() )
Point
of ( ( ) (
functional
non
empty
non
trivial
)
set
) ) &
C
: ( (
closed
) (
closed
)
Subset
of )
c=
B
: ( ( ) ( )
Subset
of ) &
B
: ( ( ) ( )
Subset
of )
c=
D
: ( (
being_simple_closed_curve
) ( non
empty
non
trivial
closed
connected
compact
bounded
being_simple_closed_curve
)
Simple_closed_curve
) ) ;