:: TOPREAL2 semantic presentation
begin
theorem
:: TOPREAL2:1
for
p1
,
p2
being ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) st
p1
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
<>
p2
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) &
p1
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
in
R^2-unit_square
: ( ( ) (
functional
non
empty
)
Element
of
K19
( the
carrier
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) ) : ( ( ) ( )
set
) ) &
p2
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
in
R^2-unit_square
: ( ( ) (
functional
non
empty
)
Element
of
K19
( the
carrier
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) ) : ( ( ) ( )
set
) ) holds
ex
P1
,
P2
being ( ( non
empty
) (
functional
non
empty
)
Subset
of ) st
(
P1
: ( ( non
empty
) (
functional
non
empty
)
Subset
of )
is_an_arc_of
p1
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) ,
p2
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) &
P2
: ( ( non
empty
) (
functional
non
empty
)
Subset
of )
is_an_arc_of
p1
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) ,
p2
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) &
R^2-unit_square
: ( ( ) (
functional
non
empty
)
Element
of
K19
( the
carrier
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
P1
: ( ( non
empty
) (
functional
non
empty
)
Subset
of )
\/
P2
: ( ( non
empty
) (
functional
non
empty
)
Subset
of ) : ( ( ) (
functional
non
empty
)
Element
of
K19
( the
carrier
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) ) : ( ( ) ( )
set
) ) &
P1
: ( ( non
empty
) (
functional
non
empty
)
Subset
of )
/\
P2
: ( ( non
empty
) (
functional
non
empty
)
Subset
of ) : ( ( ) (
functional
)
Element
of
K19
( the
carrier
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
{
p1
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) ,
p2
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
}
: ( ( ) (
functional
non
empty
)
set
) ) ;
theorem
:: TOPREAL2:2
R^2-unit_square
: ( ( ) (
functional
non
empty
)
Element
of
K19
( the
carrier
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) ) : ( ( ) ( )
set
) ) is
compact
;
theorem
:: TOPREAL2:3
for
q1
,
q2
being ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
for
Q
,
P
being ( ( non
empty
) (
functional
non
empty
)
Subset
of )
for
f
being ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
(
(
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
)
|
b
3
: ( ( non
empty
) (
functional
non
empty
)
Subset
of )
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
)
SubSpace
of
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
) ) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
(
(
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
)
|
b
4
: ( ( non
empty
) (
functional
non
empty
)
Subset
of )
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
)
SubSpace
of
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
) ) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
non
empty
total
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) st
f
: ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
(
(
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
)
|
b
3
: ( ( non
empty
) (
functional
non
empty
)
Subset
of )
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
)
SubSpace
of
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
) ) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
(
(
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
)
|
b
4
: ( ( non
empty
) (
functional
non
empty
)
Subset
of )
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
)
SubSpace
of
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
) ) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
non
empty
total
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) ) is
being_homeomorphism
&
Q
: ( ( non
empty
) (
functional
non
empty
)
Subset
of )
is_an_arc_of
q1
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) ,
q2
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) holds
for
p1
,
p2
being ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) st
p1
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
=
f
: ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
(
(
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
)
|
b
3
: ( ( non
empty
) (
functional
non
empty
)
Subset
of )
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
)
SubSpace
of
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
) ) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
(
(
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
)
|
b
4
: ( ( non
empty
) (
functional
non
empty
)
Subset
of )
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
)
SubSpace
of
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
) ) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
non
empty
total
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) )
.
q1
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) : ( ( ) ( )
set
) &
p2
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
=
f
: ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
(
(
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
)
|
b
3
: ( ( non
empty
) (
functional
non
empty
)
Subset
of )
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
)
SubSpace
of
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
) ) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
(
(
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
)
|
b
4
: ( ( non
empty
) (
functional
non
empty
)
Subset
of )
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
)
SubSpace
of
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
) ) : ( ( ) ( non
empty
)
set
)
-valued
Function-like
non
empty
total
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( non
empty
)
set
) )
.
q2
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) : ( ( ) ( )
set
) holds
P
: ( ( non
empty
) (
functional
non
empty
)
Subset
of )
is_an_arc_of
p1
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) ,
p2
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) ;
definition
let
P
be ( ( ) (
functional
)
Subset
of ) ;
attr
P
is
being_simple_closed_curve
means
:: TOPREAL2:def 1
ex
f
being ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
(
(
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
)
|
R^2-unit_square
: ( ( ) (
functional
non
empty
)
Element
of
K19
( the
carrier
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) ) : ( ( ) ( )
set
) )
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
)
SubSpace
of
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
) ) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
(
(
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
)
|
P
: ( ( ) ( )
RLTopStruct
)
)
: ( (
strict
) (
strict
TopSpace-like
)
SubSpace
of
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
) ) : ( ( ) ( )
set
)
-valued
Function-like
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( )
set
) ) st
f
: ( (
Function-like
quasi_total
) (
Relation-like
the
carrier
of
(
(
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
)
|
R^2-unit_square
: ( ( ) (
functional
non
empty
)
Element
of
K19
( the
carrier
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) ) : ( ( ) ( )
set
) )
)
: ( (
strict
) ( non
empty
strict
TopSpace-like
)
SubSpace
of
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
) ) : ( ( ) ( non
empty
)
set
)
-defined
the
carrier
of
(
(
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
)
|
P
: ( ( ) (
functional
)
Subset
of )
)
: ( (
strict
) (
strict
TopSpace-like
)
SubSpace
of
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
) ) : ( ( ) ( )
set
)
-valued
Function-like
quasi_total
)
Function
of ( ( ) ( non
empty
)
set
) , ( ( ) ( )
set
) ) is
being_homeomorphism
;
end;
registration
cluster
R^2-unit_square
: ( ( ) (
functional
non
empty
)
Element
of
K19
( the
carrier
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) ) : ( ( ) ( )
set
) )
->
being_simple_closed_curve
;
end;
registration
cluster
functional
non
empty
being_simple_closed_curve
for ( ( ) ( )
Element
of
K19
( the
carrier
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
end;
definition
mode
Simple_closed_curve
is
( (
being_simple_closed_curve
) (
functional
being_simple_closed_curve
)
Subset
of ) ;
end;
theorem
:: TOPREAL2:4
for
P
being ( ( non
empty
) (
functional
non
empty
)
Subset
of ) st
P
: ( ( non
empty
) (
functional
non
empty
)
Subset
of ) is
being_simple_closed_curve
holds
ex
p1
,
p2
being ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) st
(
p1
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
<>
p2
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) &
p1
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
in
P
: ( ( non
empty
) (
functional
non
empty
)
Subset
of ) &
p2
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
in
P
: ( ( non
empty
) (
functional
non
empty
)
Subset
of ) ) ;
theorem
:: TOPREAL2:5
for
P
being ( ( non
empty
) (
functional
non
empty
)
Subset
of ) holds
(
P
: ( ( non
empty
) (
functional
non
empty
)
Subset
of ) is
being_simple_closed_curve
iff ( ex
p1
,
p2
being ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) st
(
p1
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
<>
p2
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) &
p1
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
in
P
: ( ( non
empty
) (
functional
non
empty
)
Subset
of ) &
p2
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
in
P
: ( ( non
empty
) (
functional
non
empty
)
Subset
of ) ) & ( for
p1
,
p2
being ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) st
p1
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
<>
p2
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) &
p1
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
in
P
: ( ( non
empty
) (
functional
non
empty
)
Subset
of ) &
p2
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
in
P
: ( ( non
empty
) (
functional
non
empty
)
Subset
of ) holds
ex
P1
,
P2
being ( ( non
empty
) (
functional
non
empty
)
Subset
of ) st
(
P1
: ( ( non
empty
) (
functional
non
empty
)
Subset
of )
is_an_arc_of
p1
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) ,
p2
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) &
P2
: ( ( non
empty
) (
functional
non
empty
)
Subset
of )
is_an_arc_of
p1
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) ,
p2
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) &
P
: ( ( non
empty
) (
functional
non
empty
)
Subset
of )
=
P1
: ( ( non
empty
) (
functional
non
empty
)
Subset
of )
\/
P2
: ( ( non
empty
) (
functional
non
empty
)
Subset
of ) : ( ( ) (
functional
non
empty
)
Element
of
K19
( the
carrier
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) ) : ( ( ) ( )
set
) ) &
P1
: ( ( non
empty
) (
functional
non
empty
)
Subset
of )
/\
P2
: ( ( non
empty
) (
functional
non
empty
)
Subset
of ) : ( ( ) (
functional
)
Element
of
K19
( the
carrier
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
{
p1
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) ,
p2
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
}
: ( ( ) (
functional
non
empty
)
set
) ) ) ) ) ;
theorem
:: TOPREAL2:6
for
P
being ( ( non
empty
) (
functional
non
empty
)
Subset
of ) holds
(
P
: ( ( non
empty
) (
functional
non
empty
)
Subset
of ) is
being_simple_closed_curve
iff ex
p1
,
p2
being ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) ex
P1
,
P2
being ( ( non
empty
) (
functional
non
empty
)
Subset
of ) st
(
p1
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
<>
p2
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) &
p1
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
in
P
: ( ( non
empty
) (
functional
non
empty
)
Subset
of ) &
p2
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
in
P
: ( ( non
empty
) (
functional
non
empty
)
Subset
of ) &
P1
: ( ( non
empty
) (
functional
non
empty
)
Subset
of )
is_an_arc_of
p1
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) ,
p2
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) &
P2
: ( ( non
empty
) (
functional
non
empty
)
Subset
of )
is_an_arc_of
p1
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) ,
p2
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) &
P
: ( ( non
empty
) (
functional
non
empty
)
Subset
of )
=
P1
: ( ( non
empty
) (
functional
non
empty
)
Subset
of )
\/
P2
: ( ( non
empty
) (
functional
non
empty
)
Subset
of ) : ( ( ) (
functional
non
empty
)
Element
of
K19
( the
carrier
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) ) : ( ( ) ( )
set
) ) &
P1
: ( ( non
empty
) (
functional
non
empty
)
Subset
of )
/\
P2
: ( ( non
empty
) (
functional
non
empty
)
Subset
of ) : ( ( ) (
functional
)
Element
of
K19
( the
carrier
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) ) : ( ( ) ( )
set
) )
=
{
p1
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) ) ,
p2
: ( ( ) (
Relation-like
Function-like
V42
(2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) ) )
FinSequence-like
V154
() )
Point
of ( ( ) (
functional
non
empty
)
set
) )
}
: ( ( ) (
functional
non
empty
)
set
) ) ) ;
registration
cluster
being_simple_closed_curve
->
non
empty
compact
for ( ( ) ( )
Element
of
K19
( the
carrier
of
(
TOP-REAL
2 : ( ( ) ( non
empty
V27
()
V28
()
ext-real
positive
non
negative
V110
()
V114
()
V115
()
V162
()
V163
()
V164
()
V165
()
V166
()
V167
() )
Element
of
NAT
: ( ( ) (
V162
()
V163
()
V164
()
V165
()
V166
()
V167
()
V168
() )
Element
of
K19
(
REAL
: ( ( ) (
V162
()
V163
()
V164
()
V168
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( (
strict
) ( non
empty
TopSpace-like
T_0
T_1
T_2
V128
()
V174
()
V175
()
V176
()
V177
()
V178
()
V179
()
V180
()
strict
)
RLTopStruct
) : ( ( ) (
functional
non
empty
)
set
) ) : ( ( ) ( )
set
) ) ;
end;