begin
definition
let P be ( ( ) ( )
Subset of ) ;
let p1,
p2 be ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) ;
func x_Middle (
P,
p1,
p2)
-> ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) )
means
for
Q being ( ( ) ( )
Subset of ) st
Q : ( ( ) ( )
Subset of )
= { q : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Point of ( ( ) ( non empty functional ) set ) ) where q is ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Point of ( ( ) ( non empty functional ) set ) ) : q : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Point of ( ( ) ( non empty functional ) set ) ) `1 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) = ((p1 : ( ( Function-like quasi_total ) ( V22() V25(K7(P : ( ( ) ( ) MetrStruct ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ) V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like total quasi_total ) Element of K6(K7(K7(P : ( ( ) ( ) MetrStruct ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) `1) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) + (p2 : ( ( Function-like quasi_total ) ( V22() V25(K7(P : ( ( ) ( ) MetrStruct ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ) V26(P : ( ( ) ( ) MetrStruct ) ) Function-like quasi_total ) Element of K6(K7(K7(P : ( ( ) ( ) MetrStruct ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) `1) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) } holds
it : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) )
V26(
P : ( ( ) ( )
MetrStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
= First_Point (
P : ( ( ) ( )
MetrStruct ) ,
p1 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) )
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like total quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ,
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) )
V26(
P : ( ( ) ( )
MetrStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
Q : ( ( ) ( )
Subset of ) ) : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) ;
end;
definition
let P be ( ( ) ( )
Subset of ) ;
let p1,
p2 be ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) ;
func y_Middle (
P,
p1,
p2)
-> ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) )
means
for
Q being ( ( ) ( )
Subset of ) st
Q : ( ( ) ( )
Subset of )
= { q : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Point of ( ( ) ( non empty functional ) set ) ) where q is ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Point of ( ( ) ( non empty functional ) set ) ) : q : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Point of ( ( ) ( non empty functional ) set ) ) `2 : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) = ((p1 : ( ( Function-like quasi_total ) ( V22() V25(K7(P : ( ( ) ( ) MetrStruct ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ) V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like total quasi_total ) Element of K6(K7(K7(P : ( ( ) ( ) MetrStruct ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) `2) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) + (p2 : ( ( Function-like quasi_total ) ( V22() V25(K7(P : ( ( ) ( ) MetrStruct ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ) V26(P : ( ( ) ( ) MetrStruct ) ) Function-like quasi_total ) Element of K6(K7(K7(P : ( ( ) ( ) MetrStruct ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) `2) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) } holds
it : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) )
V26(
P : ( ( ) ( )
MetrStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
= First_Point (
P : ( ( ) ( )
MetrStruct ) ,
p1 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) )
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like total quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ,
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) )
V26(
P : ( ( ) ( )
MetrStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
Q : ( ( ) ( )
Subset of ) ) : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) ;
end;
begin
theorem
for
P being ( ( ) ( )
Subset of )
for
p1,
p2,
q1,
q2 being ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) st
P : ( ( ) ( )
Subset of )
is_an_arc_of p1 : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) ,
p2 : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) &
LE q1 : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) ,
q2 : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) ,
P : ( ( ) ( )
Subset of ) ,
p1 : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) ,
p2 : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) holds
LE q2 : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) ,
q1 : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) ,
P : ( ( ) ( )
Subset of ) ,
p2 : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) ,
p1 : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) ;
definition
let P be ( ( ) ( )
Subset of ) ;
let p1,
p2,
q1 be ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) ;
func L_Segment (
P,
p1,
p2,
q1)
-> ( ( ) ( )
Subset of )
equals
{ q : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Point of ( ( ) ( non empty functional ) set ) ) where q is ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Point of ( ( ) ( non empty functional ) set ) ) : LE q : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Point of ( ( ) ( non empty functional ) set ) ) ,q1 : ( ( Function-like quasi_total ) ( V22() V25(K7(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ) V26(P : ( ( ) ( ) MetrStruct ) ) Function-like quasi_total ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,P : ( ( ) ( ) MetrStruct ) ,p1 : ( ( Function-like quasi_total ) ( V22() V25(K7(P : ( ( ) ( ) MetrStruct ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ) V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like total quasi_total ) Element of K6(K7(K7(P : ( ( ) ( ) MetrStruct ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,p2 : ( ( Function-like quasi_total ) ( V22() V25(K7(P : ( ( ) ( ) MetrStruct ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ) V26(P : ( ( ) ( ) MetrStruct ) ) Function-like quasi_total ) Element of K6(K7(K7(P : ( ( ) ( ) MetrStruct ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) } ;
end;
definition
let P be ( ( ) ( )
Subset of ) ;
let p1,
p2,
q1 be ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) ;
func R_Segment (
P,
p1,
p2,
q1)
-> ( ( ) ( )
Subset of )
equals
{ q : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Point of ( ( ) ( non empty functional ) set ) ) where q is ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Point of ( ( ) ( non empty functional ) set ) ) : LE q1 : ( ( Function-like quasi_total ) ( V22() V25(K7(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ) V26(P : ( ( ) ( ) MetrStruct ) ) Function-like quasi_total ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,q : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Point of ( ( ) ( non empty functional ) set ) ) ,P : ( ( ) ( ) MetrStruct ) ,p1 : ( ( Function-like quasi_total ) ( V22() V25(K7(P : ( ( ) ( ) MetrStruct ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ) V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like total quasi_total ) Element of K6(K7(K7(P : ( ( ) ( ) MetrStruct ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,p2 : ( ( Function-like quasi_total ) ( V22() V25(K7(P : ( ( ) ( ) MetrStruct ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ) V26(P : ( ( ) ( ) MetrStruct ) ) Function-like quasi_total ) Element of K6(K7(K7(P : ( ( ) ( ) MetrStruct ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) } ;
end;
definition
let P be ( ( ) ( )
Subset of ) ;
let p1,
p2,
q1,
q2 be ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) ;
func Segment (
P,
p1,
p2,
q1,
q2)
-> ( ( ) ( )
Subset of )
equals
(R_Segment (P : ( ( ) ( ) MetrStruct ) ,p1 : ( ( Function-like quasi_total ) ( V22() V25(K7(P : ( ( ) ( ) MetrStruct ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ) V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like total quasi_total ) Element of K6(K7(K7(P : ( ( ) ( ) MetrStruct ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,p2 : ( ( Function-like quasi_total ) ( V22() V25(K7(P : ( ( ) ( ) MetrStruct ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ) V26(P : ( ( ) ( ) MetrStruct ) ) Function-like quasi_total ) Element of K6(K7(K7(P : ( ( ) ( ) MetrStruct ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,q1 : ( ( Function-like quasi_total ) ( V22() V25(K7(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ) V26(P : ( ( ) ( ) MetrStruct ) ) Function-like quasi_total ) Element of K6(K7(K7(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) )) : ( ( ) ( )
Subset of )
/\ (L_Segment (P : ( ( ) ( ) MetrStruct ) ,p1 : ( ( Function-like quasi_total ) ( V22() V25(K7(P : ( ( ) ( ) MetrStruct ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ) V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like total quasi_total ) Element of K6(K7(K7(P : ( ( ) ( ) MetrStruct ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,p2 : ( ( Function-like quasi_total ) ( V22() V25(K7(P : ( ( ) ( ) MetrStruct ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ) V26(P : ( ( ) ( ) MetrStruct ) ) Function-like quasi_total ) Element of K6(K7(K7(P : ( ( ) ( ) MetrStruct ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,q2 : ( ( ) ( ) Element of K6(K6(P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) )) : ( ( ) ( )
Subset of ) : ( ( ) ( )
Element of
K6( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) : ( ( ) ( )
set ) ) ;
end;
theorem
for
P being ( ( ) ( )
Subset of )
for
p1,
p2,
q1,
q2 being ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) holds
Segment (
P : ( ( ) ( )
Subset of ) ,
p1 : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) ,
p2 : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) ,
q1 : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) ,
q2 : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) ) : ( ( ) ( )
Subset of )
= { q : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Point of ( ( ) ( non empty functional ) set ) ) where q is ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Point of ( ( ) ( non empty functional ) set ) ) : ( LE q1 : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Point of ( ( ) ( non empty functional ) set ) ) ,q : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Point of ( ( ) ( non empty functional ) set ) ) ,P : ( ( ) ( ) Subset of ) ,p1 : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Point of ( ( ) ( non empty functional ) set ) ) ,p2 : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Point of ( ( ) ( non empty functional ) set ) ) & LE q : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Point of ( ( ) ( non empty functional ) set ) ) ,q2 : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Point of ( ( ) ( non empty functional ) set ) ) ,P : ( ( ) ( ) Subset of ) ,p1 : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Point of ( ( ) ( non empty functional ) set ) ) ,p2 : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Point of ( ( ) ( non empty functional ) set ) ) ) } ;
theorem
for
P being ( ( ) ( )
Subset of )
for
p1,
p2,
q1,
q2 being ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) st
P : ( ( ) ( )
Subset of )
is_an_arc_of p1 : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) ,
p2 : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) &
LE q2 : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) ,
q1 : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) ,
P : ( ( ) ( )
Subset of ) ,
p2 : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) ,
p1 : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) holds
LE q1 : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) ,
q2 : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) ,
P : ( ( ) ( )
Subset of ) ,
p1 : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) ,
p2 : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) ;
theorem
for
P being ( ( ) ( )
Subset of )
for
p1,
p2,
q1,
q2 being ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) st
P : ( ( ) ( )
Subset of )
is_an_arc_of p1 : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) ,
p2 : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) holds
Segment (
P : ( ( ) ( )
Subset of ) ,
p1 : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) ,
p2 : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) ,
q1 : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) ,
q2 : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) ) : ( ( ) ( )
Subset of )
= Segment (
P : ( ( ) ( )
Subset of ) ,
p2 : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) ,
p1 : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) ,
q2 : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) ,
q1 : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) ) : ( ( ) ( )
Subset of ) ;
begin
theorem
for
P being ( ( ) ( )
Subset of ) st
P : ( ( ) ( )
Subset of ) is
being_simple_closed_curve holds
ex
P1,
P2 being ( ( non
empty ) ( non
empty )
Subset of ) st
(
P1 : ( ( non
empty ) ( non
empty )
Subset of )
is_an_arc_of W-min P : ( ( ) ( )
Subset of ) : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) ,
E-max P : ( ( ) ( )
Subset of ) : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) &
P2 : ( ( non
empty ) ( non
empty )
Subset of )
is_an_arc_of E-max P : ( ( ) ( )
Subset of ) : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) ,
W-min P : ( ( ) ( )
Subset of ) : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) &
P1 : ( ( non
empty ) ( non
empty )
Subset of )
/\ P2 : ( ( non
empty ) ( non
empty )
Subset of ) : ( ( ) ( )
Element of
K6( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) : ( ( ) ( )
set ) )
= {(W-min P : ( ( ) ( ) Subset of ) ) : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V112() V158() V159() V160() V161() V162() V163() V164() strict V231() V232() ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) ,(E-max P : ( ( ) ( ) Subset of ) ) : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V112() V158() V159() V160() V161() V162() V163() V164() strict V231() V232() ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) } : ( ( ) ( non
empty )
set ) &
P1 : ( ( non
empty ) ( non
empty )
Subset of )
\/ P2 : ( ( non
empty ) ( non
empty )
Subset of ) : ( ( ) ( non
empty )
Element of
K6( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) : ( ( ) ( )
set ) )
= P : ( ( ) ( )
Subset of ) &
(First_Point (P1 : ( ( non empty ) ( non empty ) Subset of ) ,(W-min P : ( ( ) ( ) Subset of ) ) : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V112() V158() V159() V160() V161() V162() V163() V164() strict V231() V232() ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) ,(E-max P : ( ( ) ( ) Subset of ) ) : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V112() V158() V159() V160() V161() V162() V163() V164() strict V231() V232() ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) ,(Vertical_Line (((W-bound P : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) + (E-bound P : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) ) : ( ( ) ( ) Subset of ) )) : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
`2 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
> (Last_Point (P2 : ( ( non empty ) ( non empty ) Subset of ) ,(E-max P : ( ( ) ( ) Subset of ) ) : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V112() V158() V159() V160() V161() V162() V163() V164() strict V231() V232() ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) ,(W-min P : ( ( ) ( ) Subset of ) ) : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V112() V158() V159() V160() V161() V162() V163() V164() strict V231() V232() ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) ,(Vertical_Line (((W-bound P : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) + (E-bound P : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) ) : ( ( ) ( ) Subset of ) )) : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
`2 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) ) ;
begin
theorem
for
T,
S,
V being ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace)
for
P1 being ( ( non
empty ) ( non
empty )
Subset of )
for
P2 being ( ( ) ( )
Subset of )
for
f being ( (
Function-like quasi_total ) ( non
empty V22()
V25( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
V26( the
carrier of
(b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b4 : ( ( non empty ) ( non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) ) : ( ( ) ( non
empty )
set ) )
Function-like total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
for
g being ( (
Function-like quasi_total ) (
V22()
V25( the
carrier of
(b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b5 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) ) : ( ( ) ( )
set ) )
V26( the
carrier of
b3 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
Function-like total quasi_total )
Function of ( ( ) ( )
set ) , ( ( ) ( non
empty )
set ) ) st
P1 : ( ( non
empty ) ( non
empty )
Subset of )
c= P2 : ( ( ) ( )
Subset of ) &
f : ( (
Function-like quasi_total ) ( non
empty V22()
V25( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
V26( the
carrier of
(b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b4 : ( ( non empty ) ( non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) ) : ( ( ) ( non
empty )
set ) )
Function-like total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) is
continuous &
g : ( (
Function-like quasi_total ) (
V22()
V25( the
carrier of
(b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b5 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) ) : ( ( ) ( )
set ) )
V26( the
carrier of
b3 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
Function-like total quasi_total )
Function of ( ( ) ( )
set ) , ( ( ) ( non
empty )
set ) ) is
continuous holds
ex
h being ( (
Function-like quasi_total ) ( non
empty V22()
V25( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
V26( the
carrier of
b3 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
Function-like total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) st
(
h : ( (
Function-like quasi_total ) ( non
empty V22()
V25( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
V26( the
carrier of
b3 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
Function-like total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) )
= g : ( (
Function-like quasi_total ) (
V22()
V25( the
carrier of
(b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b5 : ( ( ) ( ) Subset of ) ) : ( (
strict ) (
strict TopSpace-like )
SubSpace of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) ) : ( ( ) ( )
set ) )
V26( the
carrier of
b3 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
Function-like total quasi_total )
Function of ( ( ) ( )
set ) , ( ( ) ( non
empty )
set ) )
* f : ( (
Function-like quasi_total ) ( non
empty V22()
V25( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
V26( the
carrier of
(b2 : ( ( non empty TopSpace-like ) ( non empty TopSpace-like ) TopSpace) | b4 : ( ( non empty ) ( non empty ) Subset of ) ) : ( (
strict ) ( non
empty strict TopSpace-like )
SubSpace of
b2 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) ) : ( ( ) ( non
empty )
set ) )
Function-like total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) : ( (
Function-like ) (
V22()
V25( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
V26( the
carrier of
b3 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
Function-like )
Element of
K6(
K7( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) , the
carrier of
b3 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) &
h : ( (
Function-like quasi_total ) ( non
empty V22()
V25( the
carrier of
b1 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
V26( the
carrier of
b3 : ( ( non
empty TopSpace-like ) ( non
empty TopSpace-like )
TopSpace) : ( ( ) ( non
empty )
set ) )
Function-like total quasi_total )
Function of ( ( ) ( non
empty )
set ) , ( ( ) ( non
empty )
set ) ) is
continuous ) ;
begin
definition
let P be ( ( ) ( )
Subset of ) ;
assume
P : ( ( ) ( )
Subset of ) is
being_simple_closed_curve
;
func Upper_Arc P -> ( ( non
empty ) ( non
empty )
Subset of )
means
(
it : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) )
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like total quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ,
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
is_an_arc_of W-min P : ( ( ) ( )
MetrStruct ) : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) ,
E-max P : ( ( ) ( )
MetrStruct ) : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) & ex
P2 being ( ( non
empty ) ( non
empty )
Subset of ) st
(
P2 : ( ( non
empty ) ( non
empty )
Subset of )
is_an_arc_of E-max P : ( ( ) ( )
MetrStruct ) : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) ,
W-min P : ( ( ) ( )
MetrStruct ) : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) &
it : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) )
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like total quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ,
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
/\ P2 : ( ( non
empty ) ( non
empty )
Subset of ) : ( ( ) ( )
Element of
K6( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) : ( ( ) ( )
set ) )
= {(W-min P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V112() V158() V159() V160() V161() V162() V163() V164() strict V231() V232() ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) ,(E-max P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V112() V158() V159() V160() V161() V162() V163() V164() strict V231() V232() ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) } : ( ( ) ( non
empty )
set ) &
it : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) )
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like total quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ,
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
\/ P2 : ( ( non
empty ) ( non
empty )
Subset of ) : ( ( ) ( non
empty )
Element of
K6( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) : ( ( ) ( )
set ) )
= P : ( ( ) ( )
MetrStruct ) &
(First_Point (it : ( ( Function-like quasi_total ) ( V22() V25(K7(P : ( ( ) ( ) MetrStruct ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ) V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like total quasi_total ) Element of K6(K7(K7(P : ( ( ) ( ) MetrStruct ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,(W-min P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V112() V158() V159() V160() V161() V162() V163() V164() strict V231() V232() ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) ,(E-max P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V112() V158() V159() V160() V161() V162() V163() V164() strict V231() V232() ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) ,(Vertical_Line (((W-bound P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) + (E-bound P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) ) : ( ( ) ( ) Subset of ) )) : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
`2 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
> (Last_Point (P2 : ( ( non empty ) ( non empty ) Subset of ) ,(E-max P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V112() V158() V159() V160() V161() V162() V163() V164() strict V231() V232() ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) ,(W-min P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V112() V158() V159() V160() V161() V162() V163() V164() strict V231() V232() ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) ,(Vertical_Line (((W-bound P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) + (E-bound P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) ) : ( ( ) ( ) Subset of ) )) : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
`2 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) ) );
end;
definition
let P be ( ( ) ( )
Subset of ) ;
assume
P : ( ( ) ( )
Subset of ) is
being_simple_closed_curve
;
func Lower_Arc P -> ( ( non
empty ) ( non
empty )
Subset of )
means
(
it : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) )
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like total quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ,
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
is_an_arc_of E-max P : ( ( ) ( )
MetrStruct ) : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) ,
W-min P : ( ( ) ( )
MetrStruct ) : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) &
(Upper_Arc P : ( ( ) ( ) MetrStruct ) ) : ( ( non
empty ) ( non
empty )
Subset of )
/\ it : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) )
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like total quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ,
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
Element of
K6( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) : ( ( ) ( )
set ) )
= {(W-min P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V112() V158() V159() V160() V161() V162() V163() V164() strict V231() V232() ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) ,(E-max P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V112() V158() V159() V160() V161() V162() V163() V164() strict V231() V232() ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) } : ( ( ) ( non
empty )
set ) &
(Upper_Arc P : ( ( ) ( ) MetrStruct ) ) : ( ( non
empty ) ( non
empty )
Subset of )
\/ it : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) )
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like total quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ,
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( non
empty )
Element of
K6( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) : ( ( ) ( )
set ) )
= P : ( ( ) ( )
MetrStruct ) &
(First_Point ((Upper_Arc P : ( ( ) ( ) MetrStruct ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(W-min P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V112() V158() V159() V160() V161() V162() V163() V164() strict V231() V232() ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) ,(E-max P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V112() V158() V159() V160() V161() V162() V163() V164() strict V231() V232() ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) ,(Vertical_Line (((W-bound P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) + (E-bound P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) ) : ( ( ) ( ) Subset of ) )) : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
`2 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
> (Last_Point (it : ( ( Function-like quasi_total ) ( V22() V25(K7(P : ( ( ) ( ) MetrStruct ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ) V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like total quasi_total ) Element of K6(K7(K7(P : ( ( ) ( ) MetrStruct ) ,P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( ) set ) ,REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ,(E-max P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V112() V158() V159() V160() V161() V162() V163() V164() strict V231() V232() ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) ,(W-min P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V112() V158() V159() V160() V161() V162() V163() V164() strict V231() V232() ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) ,(Vertical_Line (((W-bound P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) + (E-bound P : ( ( ) ( ) MetrStruct ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) ) : ( ( ) ( ) Subset of ) )) : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
`2 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) );
end;
theorem
for
P being ( ( ) ( )
Subset of ) st
P : ( ( ) ( )
Subset of ) is
being_simple_closed_curve holds
(
Upper_Arc P : ( ( ) ( )
Subset of ) : ( ( non
empty ) ( non
empty )
Subset of )
is_an_arc_of W-min P : ( ( ) ( )
Subset of ) : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) ,
E-max P : ( ( ) ( )
Subset of ) : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) &
Upper_Arc P : ( ( ) ( )
Subset of ) : ( ( non
empty ) ( non
empty )
Subset of )
is_an_arc_of E-max P : ( ( ) ( )
Subset of ) : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) ,
W-min P : ( ( ) ( )
Subset of ) : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) &
Lower_Arc P : ( ( ) ( )
Subset of ) : ( ( non
empty ) ( non
empty )
Subset of )
is_an_arc_of E-max P : ( ( ) ( )
Subset of ) : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) ,
W-min P : ( ( ) ( )
Subset of ) : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) &
Lower_Arc P : ( ( ) ( )
Subset of ) : ( ( non
empty ) ( non
empty )
Subset of )
is_an_arc_of W-min P : ( ( ) ( )
Subset of ) : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) ,
E-max P : ( ( ) ( )
Subset of ) : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) &
(Upper_Arc P : ( ( ) ( ) Subset of ) ) : ( ( non
empty ) ( non
empty )
Subset of )
/\ (Lower_Arc P : ( ( ) ( ) Subset of ) ) : ( ( non
empty ) ( non
empty )
Subset of ) : ( ( ) ( )
Element of
K6( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) : ( ( ) ( )
set ) )
= {(W-min P : ( ( ) ( ) Subset of ) ) : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V112() V158() V159() V160() V161() V162() V163() V164() strict V231() V232() ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) ,(E-max P : ( ( ) ( ) Subset of ) ) : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V112() V158() V159() V160() V161() V162() V163() V164() strict V231() V232() ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) } : ( ( ) ( non
empty )
set ) &
(Upper_Arc P : ( ( ) ( ) Subset of ) ) : ( ( non
empty ) ( non
empty )
Subset of )
\/ (Lower_Arc P : ( ( ) ( ) Subset of ) ) : ( ( non
empty ) ( non
empty )
Subset of ) : ( ( ) ( non
empty )
Element of
K6( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) : ( ( ) ( )
set ) )
= P : ( ( ) ( )
Subset of ) &
(First_Point ((Upper_Arc P : ( ( ) ( ) Subset of ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(W-min P : ( ( ) ( ) Subset of ) ) : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V112() V158() V159() V160() V161() V162() V163() V164() strict V231() V232() ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) ,(E-max P : ( ( ) ( ) Subset of ) ) : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V112() V158() V159() V160() V161() V162() V163() V164() strict V231() V232() ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) ,(Vertical_Line (((W-bound P : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) + (E-bound P : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) ) : ( ( ) ( ) Subset of ) )) : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
`2 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
> (Last_Point ((Lower_Arc P : ( ( ) ( ) Subset of ) ) : ( ( non empty ) ( non empty ) Subset of ) ,(E-max P : ( ( ) ( ) Subset of ) ) : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V112() V158() V159() V160() V161() V162() V163() V164() strict V231() V232() ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) ,(W-min P : ( ( ) ( ) Subset of ) ) : ( ( ) ( V22() V26( REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) Function-like V43(2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V138() ) Element of the carrier of (TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( strict ) ( non empty TopSpace-like T_0 T_1 T_2 V112() V158() V159() V160() V161() V162() V163() V164() strict V231() V232() ) RLTopStruct ) : ( ( ) ( non empty functional ) set ) ) ,(Vertical_Line (((W-bound P : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) + (E-bound P : ( ( ) ( ) Subset of ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) / 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V11() real ext-real ) Element of REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) ) : ( ( ) ( ) Subset of ) )) : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) )
`2 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) ) ;
begin
definition
let P be ( ( ) ( )
Subset of ) ;
let q1,
q2 be ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Point of ( ( ) ( non
empty functional )
set ) ) ;
pred LE q1,
q2,
P means
( (
q1 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) )
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like total quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ,
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
in Upper_Arc P : ( ( ) ( )
MetrStruct ) : ( ( non
empty ) ( non
empty )
Subset of ) &
q2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) )
V26(
P : ( ( ) ( )
MetrStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
in Lower_Arc P : ( ( ) ( )
MetrStruct ) : ( ( non
empty ) ( non
empty )
Subset of ) & not
q2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) )
V26(
P : ( ( ) ( )
MetrStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
= W-min P : ( ( ) ( )
MetrStruct ) : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) ) or (
q1 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) )
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like total quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ,
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
in Upper_Arc P : ( ( ) ( )
MetrStruct ) : ( ( non
empty ) ( non
empty )
Subset of ) &
q2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) )
V26(
P : ( ( ) ( )
MetrStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
in Upper_Arc P : ( ( ) ( )
MetrStruct ) : ( ( non
empty ) ( non
empty )
Subset of ) &
LE q1 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) )
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like total quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ,
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
q2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) )
V26(
P : ( ( ) ( )
MetrStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
Upper_Arc P : ( ( ) ( )
MetrStruct ) : ( ( non
empty ) ( non
empty )
Subset of ) ,
W-min P : ( ( ) ( )
MetrStruct ) : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) ,
E-max P : ( ( ) ( )
MetrStruct ) : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) ) or (
q1 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) )
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like total quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ,
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
in Lower_Arc P : ( ( ) ( )
MetrStruct ) : ( ( non
empty ) ( non
empty )
Subset of ) &
q2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) )
V26(
P : ( ( ) ( )
MetrStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
in Lower_Arc P : ( ( ) ( )
MetrStruct ) : ( ( non
empty ) ( non
empty )
Subset of ) & not
q2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) )
V26(
P : ( ( ) ( )
MetrStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) )
= W-min P : ( ( ) ( )
MetrStruct ) : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) &
LE q1 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) )
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like total quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ,
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
q2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) )
V26(
P : ( ( ) ( )
MetrStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
MetrStruct ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ,
P : ( ( ) ( )
MetrStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
Lower_Arc P : ( ( ) ( )
MetrStruct ) : ( ( non
empty ) ( non
empty )
Subset of ) ,
E-max P : ( ( ) ( )
MetrStruct ) : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) ,
W-min P : ( ( ) ( )
MetrStruct ) : ( ( ) (
V22()
V26(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) )
Function-like V43(2 : ( ( ) ( non
empty natural V11()
real ext-real positive non
negative V83()
V84()
V146()
V147()
V148()
V149()
V150()
V151() )
Element of
NAT : ( ( ) (
V146()
V147()
V148()
V149()
V150()
V151()
V152()
V181() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V146()
V147()
V148()
V152()
V181() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V138() )
Element of the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real positive non negative V83() V84() V146() V147() V148() V149() V150() V151() ) Element of NAT : ( ( ) ( V146() V147() V148() V149() V150() V151() V152() V181() ) Element of K6(REAL : ( ( ) ( non empty V36() V146() V147() V148() V152() V181() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_0 T_1 T_2 V112()
V158()
V159()
V160()
V161()
V162()
V163()
V164()
strict V231()
V232() )
RLTopStruct ) : ( ( ) ( non
empty functional )
set ) ) ) );
end;