begin
theorem
for
n being ( ( ) (
natural V11()
real ext-real V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) )
for
a,
p1,
p2 being ( ( ) (
V43(
b1 : ( ( ) (
natural V11()
real ext-real V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) )
for
P being ( ( ) ( )
Subset of ) st
a : ( ( ) (
V43(
b1 : ( ( ) (
natural V11()
real ext-real V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) )
in P : ( ( ) ( )
Subset of ) &
P : ( ( ) ( )
Subset of )
is_an_arc_of p1 : ( ( ) (
V43(
b1 : ( ( ) (
natural V11()
real ext-real V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) ,
p2 : ( ( ) (
V43(
b1 : ( ( ) (
natural V11()
real ext-real V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) holds
ex
f being ( (
Function-like V33( the
carrier of
I[01] : ( ( ) ( )
TopStruct ) : ( ( ) ( )
set ) , the
carrier of
((TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) | b5 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict )
SubSpace of
TOP-REAL b1 : ( ( ) (
natural V11()
real ext-real V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
V186() ) ( non
empty TopSpace-like V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) ) : ( ( ) ( )
set ) ) ) (
Relation-like the
carrier of
I[01] : ( ( ) ( )
TopStruct ) : ( ( ) ( )
set )
-defined the
carrier of
((TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) | b5 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict )
SubSpace of
TOP-REAL b1 : ( ( ) (
natural V11()
real ext-real V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
V186() ) ( non
empty TopSpace-like V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) ) : ( ( ) ( )
set )
-valued Function-like V33( the
carrier of
I[01] : ( ( ) ( )
TopStruct ) : ( ( ) ( )
set ) , the
carrier of
((TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) | b5 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict )
SubSpace of
TOP-REAL b1 : ( ( ) (
natural V11()
real ext-real V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
V186() ) ( non
empty TopSpace-like V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) ) : ( ( ) ( )
set ) ) )
Function of ( ( ) ( )
set ) , ( ( ) ( )
set ) ) ex
r being ( ( ) (
V11()
real ext-real )
Real) st
(
f : ( (
Function-like V33( the
carrier of
I[01] : ( ( ) ( )
TopStruct ) : ( ( ) ( )
set ) , the
carrier of
((TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) | b5 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict )
SubSpace of
TOP-REAL b1 : ( ( ) (
natural V11()
real ext-real V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
V186() ) ( non
empty TopSpace-like V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) ) : ( ( ) ( )
set ) ) ) (
Relation-like the
carrier of
I[01] : ( ( ) ( )
TopStruct ) : ( ( ) ( )
set )
-defined the
carrier of
((TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) | b5 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict )
SubSpace of
TOP-REAL b1 : ( ( ) (
natural V11()
real ext-real V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
V186() ) ( non
empty TopSpace-like V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) ) : ( ( ) ( )
set )
-valued Function-like V33( the
carrier of
I[01] : ( ( ) ( )
TopStruct ) : ( ( ) ( )
set ) , the
carrier of
((TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) | b5 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict )
SubSpace of
TOP-REAL b1 : ( ( ) (
natural V11()
real ext-real V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
V186() ) ( non
empty TopSpace-like V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) ) : ( ( ) ( )
set ) ) )
Function of ( ( ) ( )
set ) , ( ( ) ( )
set ) ) is
being_homeomorphism &
f : ( (
Function-like V33( the
carrier of
I[01] : ( ( ) ( )
TopStruct ) : ( ( ) ( )
set ) , the
carrier of
((TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) | b5 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict )
SubSpace of
TOP-REAL b1 : ( ( ) (
natural V11()
real ext-real V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
V186() ) ( non
empty TopSpace-like V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) ) : ( ( ) ( )
set ) ) ) (
Relation-like the
carrier of
I[01] : ( ( ) ( )
TopStruct ) : ( ( ) ( )
set )
-defined the
carrier of
((TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) | b5 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict )
SubSpace of
TOP-REAL b1 : ( ( ) (
natural V11()
real ext-real V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
V186() ) ( non
empty TopSpace-like V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) ) : ( ( ) ( )
set )
-valued Function-like V33( the
carrier of
I[01] : ( ( ) ( )
TopStruct ) : ( ( ) ( )
set ) , the
carrier of
((TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) | b5 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict )
SubSpace of
TOP-REAL b1 : ( ( ) (
natural V11()
real ext-real V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
V186() ) ( non
empty TopSpace-like V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) ) : ( ( ) ( )
set ) ) )
Function of ( ( ) ( )
set ) , ( ( ) ( )
set ) )
. 0 : ( ( ) (
natural V11()
real ext-real V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) ( )
set )
= p1 : ( ( ) (
V43(
b1 : ( ( ) (
natural V11()
real ext-real V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) &
f : ( (
Function-like V33( the
carrier of
I[01] : ( ( ) ( )
TopStruct ) : ( ( ) ( )
set ) , the
carrier of
((TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) | b5 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict )
SubSpace of
TOP-REAL b1 : ( ( ) (
natural V11()
real ext-real V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
V186() ) ( non
empty TopSpace-like V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) ) : ( ( ) ( )
set ) ) ) (
Relation-like the
carrier of
I[01] : ( ( ) ( )
TopStruct ) : ( ( ) ( )
set )
-defined the
carrier of
((TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) | b5 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict )
SubSpace of
TOP-REAL b1 : ( ( ) (
natural V11()
real ext-real V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
V186() ) ( non
empty TopSpace-like V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) ) : ( ( ) ( )
set )
-valued Function-like V33( the
carrier of
I[01] : ( ( ) ( )
TopStruct ) : ( ( ) ( )
set ) , the
carrier of
((TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) | b5 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict )
SubSpace of
TOP-REAL b1 : ( ( ) (
natural V11()
real ext-real V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
V186() ) ( non
empty TopSpace-like V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) ) : ( ( ) ( )
set ) ) )
Function of ( ( ) ( )
set ) , ( ( ) ( )
set ) )
. 1 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) : ( ( ) ( )
set )
= p2 : ( ( ) (
V43(
b1 : ( ( ) (
natural V11()
real ext-real V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) &
0 : ( ( ) (
natural V11()
real ext-real V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) )
<= r : ( ( ) (
V11()
real ext-real )
Real) &
r : ( ( ) (
V11()
real ext-real )
Real)
<= 1 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) &
f : ( (
Function-like V33( the
carrier of
I[01] : ( ( ) ( )
TopStruct ) : ( ( ) ( )
set ) , the
carrier of
((TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) | b5 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict )
SubSpace of
TOP-REAL b1 : ( ( ) (
natural V11()
real ext-real V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
V186() ) ( non
empty TopSpace-like V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) ) : ( ( ) ( )
set ) ) ) (
Relation-like the
carrier of
I[01] : ( ( ) ( )
TopStruct ) : ( ( ) ( )
set )
-defined the
carrier of
((TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) | b5 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict )
SubSpace of
TOP-REAL b1 : ( ( ) (
natural V11()
real ext-real V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
V186() ) ( non
empty TopSpace-like V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) ) : ( ( ) ( )
set )
-valued Function-like V33( the
carrier of
I[01] : ( ( ) ( )
TopStruct ) : ( ( ) ( )
set ) , the
carrier of
((TOP-REAL b1 : ( ( ) ( natural V11() real ext-real V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( V186() ) ( non empty TopSpace-like V128() V174() V175() V176() V177() V178() V179() V180() V186() ) L15()) | b5 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict )
SubSpace of
TOP-REAL b1 : ( ( ) (
natural V11()
real ext-real V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
V186() ) ( non
empty TopSpace-like V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) ) : ( ( ) ( )
set ) ) )
Function of ( ( ) ( )
set ) , ( ( ) ( )
set ) )
. r : ( ( ) (
V11()
real ext-real )
Real) : ( ( ) ( )
set )
= a : ( ( ) (
V43(
b1 : ( ( ) (
natural V11()
real ext-real V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) ) ;
theorem
for
a,
b,
c,
d being ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) )
for
P being ( ( ) ( )
Subset of ) st
a : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) )
<> b : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) &
P : ( ( ) ( )
Subset of )
is_an_arc_of c : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) ,
d : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) &
LE a : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) ,
b : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) ,
P : ( ( ) ( )
Subset of ) ,
c : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) ,
d : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) holds
ex
e being ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) st
(
a : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) )
<> e : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) &
b : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) )
<> e : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) &
LE a : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) ,
e : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) ,
P : ( ( ) ( )
Subset of ) ,
c : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) ,
d : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) &
LE e : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) ,
b : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) ,
P : ( ( ) ( )
Subset of ) ,
c : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) ,
d : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) ) ;
definition
let P be ( ( ) ( )
Subset of ) ;
let a,
b,
c,
d be ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) ;
pred a,
b,
c,
d are_in_this_order_on P means
( (
LE a : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
b : ( ( ) ( )
Element of
P : ( ( ) ( )
TopStruct ) ) ,
P : ( ( ) ( )
TopStruct ) &
LE b : ( ( ) ( )
Element of
P : ( ( ) ( )
TopStruct ) ) ,
c : ( ( ) ( )
set ) ,
P : ( ( ) ( )
TopStruct ) &
LE c : ( ( ) ( )
set ) ,
d : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
V186() ) ( non
empty TopSpace-like V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) : ( ( ) ( )
set ) ) ,
P : ( ( ) ( )
TopStruct ) ) or (
LE b : ( ( ) ( )
Element of
P : ( ( ) ( )
TopStruct ) ) ,
c : ( ( ) ( )
set ) ,
P : ( ( ) ( )
TopStruct ) &
LE c : ( ( ) ( )
set ) ,
d : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
V186() ) ( non
empty TopSpace-like V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) : ( ( ) ( )
set ) ) ,
P : ( ( ) ( )
TopStruct ) &
LE d : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
V186() ) ( non
empty TopSpace-like V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) : ( ( ) ( )
set ) ) ,
a : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
P : ( ( ) ( )
TopStruct ) ) or (
LE c : ( ( ) ( )
set ) ,
d : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
V186() ) ( non
empty TopSpace-like V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) : ( ( ) ( )
set ) ) ,
P : ( ( ) ( )
TopStruct ) &
LE d : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
V186() ) ( non
empty TopSpace-like V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) : ( ( ) ( )
set ) ) ,
a : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
P : ( ( ) ( )
TopStruct ) &
LE a : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
b : ( ( ) ( )
Element of
P : ( ( ) ( )
TopStruct ) ) ,
P : ( ( ) ( )
TopStruct ) ) or (
LE d : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( V1() natural V11() real ext-real positive V114() V115() V162() V163() V164() V165() V166() V167() ) Element of NAT : ( ( ) ( V162() V163() V164() V165() V166() V167() V168() ) Element of K6(REAL : ( ( ) ( V162() V163() V164() V168() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
V186() ) ( non
empty TopSpace-like V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) : ( ( ) ( )
set ) ) ,
a : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
P : ( ( ) ( )
TopStruct ) &
LE a : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
b : ( ( ) ( )
Element of
P : ( ( ) ( )
TopStruct ) ) ,
P : ( ( ) ( )
TopStruct ) &
LE b : ( ( ) ( )
Element of
P : ( ( ) ( )
TopStruct ) ) ,
c : ( ( ) ( )
set ) ,
P : ( ( ) ( )
TopStruct ) ) );
end;
theorem
for
C being ( (
being_simple_closed_curve ) (
V1()
V75(
TOP-REAL 2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
V186() ) ( non
empty TopSpace-like V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) )
being_simple_closed_curve )
Simple_closed_curve)
for
a,
b,
c,
d being ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) st
a : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) )
in C : ( (
being_simple_closed_curve ) (
V1()
V75(
TOP-REAL 2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
V186() ) ( non
empty TopSpace-like V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) )
being_simple_closed_curve )
Simple_closed_curve) &
b : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) )
in C : ( (
being_simple_closed_curve ) (
V1()
V75(
TOP-REAL 2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
V186() ) ( non
empty TopSpace-like V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) )
being_simple_closed_curve )
Simple_closed_curve) &
c : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) )
in C : ( (
being_simple_closed_curve ) (
V1()
V75(
TOP-REAL 2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
V186() ) ( non
empty TopSpace-like V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) )
being_simple_closed_curve )
Simple_closed_curve) &
d : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) )
in C : ( (
being_simple_closed_curve ) (
V1()
V75(
TOP-REAL 2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
V186() ) ( non
empty TopSpace-like V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) )
being_simple_closed_curve )
Simple_closed_curve) & not
a : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) ,
b : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) ,
c : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) ,
d : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) )
are_in_this_order_on C : ( (
being_simple_closed_curve ) (
V1()
V75(
TOP-REAL 2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
V186() ) ( non
empty TopSpace-like V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) )
being_simple_closed_curve )
Simple_closed_curve) & not
a : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) ,
b : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) ,
d : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) ,
c : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) )
are_in_this_order_on C : ( (
being_simple_closed_curve ) (
V1()
V75(
TOP-REAL 2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
V186() ) ( non
empty TopSpace-like V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) )
being_simple_closed_curve )
Simple_closed_curve) & not
a : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) ,
c : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) ,
b : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) ,
d : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) )
are_in_this_order_on C : ( (
being_simple_closed_curve ) (
V1()
V75(
TOP-REAL 2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
V186() ) ( non
empty TopSpace-like V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) )
being_simple_closed_curve )
Simple_closed_curve) & not
a : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) ,
c : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) ,
d : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) ,
b : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) )
are_in_this_order_on C : ( (
being_simple_closed_curve ) (
V1()
V75(
TOP-REAL 2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
V186() ) ( non
empty TopSpace-like V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) )
being_simple_closed_curve )
Simple_closed_curve) & not
a : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) ,
d : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) ,
b : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) ,
c : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) )
are_in_this_order_on C : ( (
being_simple_closed_curve ) (
V1()
V75(
TOP-REAL 2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
V186() ) ( non
empty TopSpace-like V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) )
being_simple_closed_curve )
Simple_closed_curve) holds
a : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) ,
d : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) ,
c : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) ) ,
b : ( ( ) (
V43(2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) )
V111()
V154() )
Point of ( ( ) ( )
set ) )
are_in_this_order_on C : ( (
being_simple_closed_curve ) (
V1()
V75(
TOP-REAL 2 : ( ( ) (
V1()
natural V11()
real ext-real positive V114()
V115()
V162()
V163()
V164()
V165()
V166()
V167() )
Element of
NAT : ( ( ) (
V162()
V163()
V164()
V165()
V166()
V167()
V168() )
Element of
K6(
REAL : ( ( ) (
V162()
V163()
V164()
V168() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
V186() ) ( non
empty TopSpace-like V128()
V174()
V175()
V176()
V177()
V178()
V179()
V180()
V186() )
L15()) )
being_simple_closed_curve )
Simple_closed_curve) ;