begin
definition
let P be ( ( ) ( )
Subset of ) ;
let p1,
p2,
p be ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ;
let e be ( ( ) (
V11()
real ext-real )
Real) ;
pred p is_Lin P,
p1,
p2,
e means
(
P : ( ( ) ( )
TopStruct )
is_an_arc_of p1 : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) &
p : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) )
in P : ( ( ) ( )
TopStruct ) &
p : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) )
= e : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) & ex
p4 being ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) st
(
p4 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) )
< e : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) &
LE p4 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) ,
P : ( ( ) ( )
TopStruct ) ,
p1 : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) & ( for
p5 being ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) st
LE p4 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p5 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
P : ( ( ) ( )
TopStruct ) ,
p1 : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) &
LE p5 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) ,
P : ( ( ) ( )
TopStruct ) ,
p1 : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) holds
p5 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) )
<= e : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) ) );
pred p is_Rin P,
p1,
p2,
e means
(
P : ( ( ) ( )
TopStruct )
is_an_arc_of p1 : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) &
p : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) )
in P : ( ( ) ( )
TopStruct ) &
p : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) )
= e : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) & ex
p4 being ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) st
(
p4 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) )
> e : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) &
LE p4 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) ,
P : ( ( ) ( )
TopStruct ) ,
p1 : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) & ( for
p5 being ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) st
LE p4 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p5 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
P : ( ( ) ( )
TopStruct ) ,
p1 : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) &
LE p5 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) ,
P : ( ( ) ( )
TopStruct ) ,
p1 : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) holds
p5 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) )
>= e : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) ) );
pred p is_Lout P,
p1,
p2,
e means
(
P : ( ( ) ( )
TopStruct )
is_an_arc_of p1 : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) &
p : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) )
in P : ( ( ) ( )
TopStruct ) &
p : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) )
= e : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) & ex
p4 being ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) st
(
p4 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) )
< e : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) &
LE p : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) ,
p4 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
P : ( ( ) ( )
TopStruct ) ,
p1 : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) & ( for
p5 being ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) st
LE p5 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p4 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
P : ( ( ) ( )
TopStruct ) ,
p1 : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) &
LE p : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) ,
p5 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
P : ( ( ) ( )
TopStruct ) ,
p1 : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) holds
p5 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) )
<= e : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) ) );
pred p is_Rout P,
p1,
p2,
e means
(
P : ( ( ) ( )
TopStruct )
is_an_arc_of p1 : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) &
p : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) )
in P : ( ( ) ( )
TopStruct ) &
p : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) )
= e : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) & ex
p4 being ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) st
(
p4 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) )
> e : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) &
LE p : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) ,
p4 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
P : ( ( ) ( )
TopStruct ) ,
p1 : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) & ( for
p5 being ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) st
LE p5 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p4 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
P : ( ( ) ( )
TopStruct ) ,
p1 : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) &
LE p : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) ,
p5 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
P : ( ( ) ( )
TopStruct ) ,
p1 : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) holds
p5 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) )
>= e : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) ) );
pred p is_OSin P,
p1,
p2,
e means
(
P : ( ( ) ( )
TopStruct )
is_an_arc_of p1 : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) &
p : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) )
in P : ( ( ) ( )
TopStruct ) &
p : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) )
= e : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) & ex
p7 being ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) st
(
LE p7 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) ,
P : ( ( ) ( )
TopStruct ) ,
p1 : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) & ( for
p8 being ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) st
LE p7 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p8 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
P : ( ( ) ( )
TopStruct ) ,
p1 : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) &
LE p8 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) ,
P : ( ( ) ( )
TopStruct ) ,
p1 : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) holds
p8 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) )
= e : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) & ( for
p4 being ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) st
LE p4 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p7 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
P : ( ( ) ( )
TopStruct ) ,
p1 : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) &
p4 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
<> p7 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) holds
( ex
p5 being ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) st
(
LE p4 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p5 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
P : ( ( ) ( )
TopStruct ) ,
p1 : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) &
LE p5 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p7 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
P : ( ( ) ( )
TopStruct ) ,
p1 : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) &
p5 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) )
> e : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) & ex
p6 being ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) st
(
LE p4 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p6 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
P : ( ( ) ( )
TopStruct ) ,
p1 : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) &
LE p6 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p7 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
P : ( ( ) ( )
TopStruct ) ,
p1 : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) &
p6 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) )
< e : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) ) ) ) );
pred p is_OSout P,
p1,
p2,
e means
(
P : ( ( ) ( )
TopStruct )
is_an_arc_of p1 : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) &
p : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) )
in P : ( ( ) ( )
TopStruct ) &
p : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) )
= e : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) & ex
p7 being ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) st
(
LE p : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) ,
p7 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
P : ( ( ) ( )
TopStruct ) ,
p1 : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) & ( for
p8 being ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) st
LE p8 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p7 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
P : ( ( ) ( )
TopStruct ) ,
p1 : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) &
LE p : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) ,
p8 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
P : ( ( ) ( )
TopStruct ) ,
p1 : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) holds
p8 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) )
= e : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) & ( for
p4 being ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) st
LE p7 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p4 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
P : ( ( ) ( )
TopStruct ) ,
p1 : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) &
p4 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
<> p7 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) holds
( ex
p5 being ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) st
(
LE p5 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p4 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
P : ( ( ) ( )
TopStruct ) ,
p1 : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) &
LE p7 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p5 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
P : ( ( ) ( )
TopStruct ) ,
p1 : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) &
p5 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) )
> e : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) & ex
p6 being ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) st
(
LE p6 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p4 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
P : ( ( ) ( )
TopStruct ) ,
p1 : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) &
LE p7 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p6 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
P : ( ( ) ( )
TopStruct ) ,
p1 : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ,
p2 : ( (
Function-like quasi_total ) (
V22()
V25(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) )
V26(
P : ( ( ) ( )
TopStruct ) )
Function-like quasi_total )
Element of
K6(
K7(
K7(
P : ( ( ) ( )
TopStruct ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ,
P : ( ( ) ( )
TopStruct ) ) : ( ( ) (
V22() )
set ) ) : ( ( ) ( )
set ) ) &
p6 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) )
< e : ( ( ) ( )
Element of
K6(
K6(
P : ( ( ) ( )
TopStruct ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
set ) ) ) ) ) ) );
end;
theorem
for
P being ( ( non
empty ) ( non
empty )
Subset of )
for
p1,
p2,
p being ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
for
e being ( ( ) (
V11()
real ext-real )
Real) st
P : ( ( non
empty ) ( non
empty )
Subset of )
is_an_arc_of p1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) &
p1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) )
< e : ( ( ) (
V11()
real ext-real )
Real) &
p : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
in P : ( ( non
empty ) ( non
empty )
Subset of ) &
p : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) )
= e : ( ( ) (
V11()
real ext-real )
Real) & not
p : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
is_Lin P : ( ( non
empty ) ( non
empty )
Subset of ) ,
p1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
e : ( ( ) (
V11()
real ext-real )
Real) & not
p : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
is_Rin P : ( ( non
empty ) ( non
empty )
Subset of ) ,
p1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
e : ( ( ) (
V11()
real ext-real )
Real) holds
p : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
is_OSin P : ( ( non
empty ) ( non
empty )
Subset of ) ,
p1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
e : ( ( ) (
V11()
real ext-real )
Real) ;
theorem
for
P being ( ( non
empty ) ( non
empty )
Subset of )
for
p1,
p2,
p being ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
for
e being ( ( ) (
V11()
real ext-real )
Real) st
P : ( ( non
empty ) ( non
empty )
Subset of )
is_an_arc_of p1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) &
p2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) )
> e : ( ( ) (
V11()
real ext-real )
Real) &
p : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
in P : ( ( non
empty ) ( non
empty )
Subset of ) &
p : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) )
= e : ( ( ) (
V11()
real ext-real )
Real) & not
p : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
is_Lout P : ( ( non
empty ) ( non
empty )
Subset of ) ,
p1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
e : ( ( ) (
V11()
real ext-real )
Real) & not
p : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
is_Rout P : ( ( non
empty ) ( non
empty )
Subset of ) ,
p1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
e : ( ( ) (
V11()
real ext-real )
Real) holds
p : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
is_OSout P : ( ( non
empty ) ( non
empty )
Subset of ) ,
p1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
e : ( ( ) (
V11()
real ext-real )
Real) ;
theorem
for
P being ( ( non
empty ) ( non
empty )
Subset of )
for
p1,
p2,
q1,
q2 being ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) st
P : ( ( non
empty ) ( non
empty )
Subset of )
is_an_arc_of p1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) &
q1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
in P : ( ( non
empty ) ( non
empty )
Subset of ) &
q2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
in P : ( ( non
empty ) ( non
empty )
Subset of ) & not
LE q1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
q2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
P : ( ( non
empty ) ( non
empty )
Subset of ) ,
p1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) holds
LE q2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
q1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
P : ( ( non
empty ) ( non
empty )
Subset of ) ,
p1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ;
theorem
for
P being ( ( non
empty ) ( non
empty )
Subset of )
for
p1,
p2,
q1,
q2,
q3 being ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) st
P : ( ( non
empty ) ( non
empty )
Subset of )
is_an_arc_of p1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) &
LE q1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
q2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
P : ( ( non
empty ) ( non
empty )
Subset of ) ,
p1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) &
LE q2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
q3 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
P : ( ( non
empty ) ( non
empty )
Subset of ) ,
p1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) holds
(Segment (P : ( ( non empty ) ( non empty ) Subset of ) ,p1 : ( ( ) ( V43(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below ) Element of NAT : ( ( ) ( V143() V144() V145() V146() V147() V148() V149() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V36() V143() V144() V145() V149() non bounded_below non bounded_above V209() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V135() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V43(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below ) Element of NAT : ( ( ) ( V143() V144() V145() V146() V147() V148() V149() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V36() V143() V144() V145() V149() non bounded_below non bounded_above V209() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V135() ) Point of ( ( ) ( non empty ) set ) ) ,q1 : ( ( ) ( V43(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below ) Element of NAT : ( ( ) ( V143() V144() V145() V146() V147() V148() V149() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V36() V143() V144() V145() V149() non bounded_below non bounded_above V209() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V135() ) Point of ( ( ) ( non empty ) set ) ) ,q2 : ( ( ) ( V43(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below ) Element of NAT : ( ( ) ( V143() V144() V145() V146() V147() V148() V149() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V36() V143() V144() V145() V149() non bounded_below non bounded_above V209() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V135() ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( )
Element of
K6( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below ) Element of NAT : ( ( ) ( V143() V144() V145() V146() V147() V148() V149() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V36() V143() V144() V145() V149() non bounded_below non bounded_above V209() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like V109()
V155()
V156()
V157()
V158()
V159()
V160()
V161()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) )
\/ (Segment (P : ( ( non empty ) ( non empty ) Subset of ) ,p1 : ( ( ) ( V43(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below ) Element of NAT : ( ( ) ( V143() V144() V145() V146() V147() V148() V149() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V36() V143() V144() V145() V149() non bounded_below non bounded_above V209() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V135() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V43(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below ) Element of NAT : ( ( ) ( V143() V144() V145() V146() V147() V148() V149() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V36() V143() V144() V145() V149() non bounded_below non bounded_above V209() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V135() ) Point of ( ( ) ( non empty ) set ) ) ,q2 : ( ( ) ( V43(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below ) Element of NAT : ( ( ) ( V143() V144() V145() V146() V147() V148() V149() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V36() V143() V144() V145() V149() non bounded_below non bounded_above V209() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V135() ) Point of ( ( ) ( non empty ) set ) ) ,q3 : ( ( ) ( V43(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below ) Element of NAT : ( ( ) ( V143() V144() V145() V146() V147() V148() V149() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V36() V143() V144() V145() V149() non bounded_below non bounded_above V209() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V135() ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( )
Element of
K6( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below ) Element of NAT : ( ( ) ( V143() V144() V145() V146() V147() V148() V149() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V36() V143() V144() V145() V149() non bounded_below non bounded_above V209() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like V109()
V155()
V156()
V157()
V158()
V159()
V160()
V161()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
Element of
K6( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below ) Element of NAT : ( ( ) ( V143() V144() V145() V146() V147() V148() V149() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V36() V143() V144() V145() V149() non bounded_below non bounded_above V209() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like V109()
V155()
V156()
V157()
V158()
V159()
V160()
V161()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) )
= Segment (
P : ( ( non
empty ) ( non
empty )
Subset of ) ,
p1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
q1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
q3 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Element of
K6( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below ) Element of NAT : ( ( ) ( V143() V144() V145() V146() V147() V148() V149() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V36() V143() V144() V145() V149() non bounded_below non bounded_above V209() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like V109()
V155()
V156()
V157()
V158()
V159()
V160()
V161()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ) ;
theorem
for
P being ( ( non
empty ) ( non
empty )
Subset of )
for
p1,
p2,
q1,
q2,
q3 being ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) st
P : ( ( non
empty ) ( non
empty )
Subset of )
is_an_arc_of p1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) &
LE q1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
q2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
P : ( ( non
empty ) ( non
empty )
Subset of ) ,
p1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) &
LE q2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
q3 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
P : ( ( non
empty ) ( non
empty )
Subset of ) ,
p1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) holds
(Segment (P : ( ( non empty ) ( non empty ) Subset of ) ,p1 : ( ( ) ( V43(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below ) Element of NAT : ( ( ) ( V143() V144() V145() V146() V147() V148() V149() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V36() V143() V144() V145() V149() non bounded_below non bounded_above V209() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V135() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V43(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below ) Element of NAT : ( ( ) ( V143() V144() V145() V146() V147() V148() V149() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V36() V143() V144() V145() V149() non bounded_below non bounded_above V209() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V135() ) Point of ( ( ) ( non empty ) set ) ) ,q1 : ( ( ) ( V43(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below ) Element of NAT : ( ( ) ( V143() V144() V145() V146() V147() V148() V149() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V36() V143() V144() V145() V149() non bounded_below non bounded_above V209() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V135() ) Point of ( ( ) ( non empty ) set ) ) ,q2 : ( ( ) ( V43(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below ) Element of NAT : ( ( ) ( V143() V144() V145() V146() V147() V148() V149() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V36() V143() V144() V145() V149() non bounded_below non bounded_above V209() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V135() ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( )
Element of
K6( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below ) Element of NAT : ( ( ) ( V143() V144() V145() V146() V147() V148() V149() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V36() V143() V144() V145() V149() non bounded_below non bounded_above V209() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like V109()
V155()
V156()
V157()
V158()
V159()
V160()
V161()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) )
/\ (Segment (P : ( ( non empty ) ( non empty ) Subset of ) ,p1 : ( ( ) ( V43(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below ) Element of NAT : ( ( ) ( V143() V144() V145() V146() V147() V148() V149() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V36() V143() V144() V145() V149() non bounded_below non bounded_above V209() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V135() ) Point of ( ( ) ( non empty ) set ) ) ,p2 : ( ( ) ( V43(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below ) Element of NAT : ( ( ) ( V143() V144() V145() V146() V147() V148() V149() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V36() V143() V144() V145() V149() non bounded_below non bounded_above V209() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V135() ) Point of ( ( ) ( non empty ) set ) ) ,q2 : ( ( ) ( V43(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below ) Element of NAT : ( ( ) ( V143() V144() V145() V146() V147() V148() V149() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V36() V143() V144() V145() V149() non bounded_below non bounded_above V209() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V135() ) Point of ( ( ) ( non empty ) set ) ) ,q3 : ( ( ) ( V43(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below ) Element of NAT : ( ( ) ( V143() V144() V145() V146() V147() V148() V149() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V36() V143() V144() V145() V149() non bounded_below non bounded_above V209() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V135() ) Point of ( ( ) ( non empty ) set ) ) )) : ( ( ) ( )
Element of
K6( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below ) Element of NAT : ( ( ) ( V143() V144() V145() V146() V147() V148() V149() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V36() V143() V144() V145() V149() non bounded_below non bounded_above V209() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like V109()
V155()
V156()
V157()
V158()
V159()
V160()
V161()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ) : ( ( ) ( )
Element of
K6( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below ) Element of NAT : ( ( ) ( V143() V144() V145() V146() V147() V148() V149() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V36() V143() V144() V145() V149() non bounded_below non bounded_above V209() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like V109()
V155()
V156()
V157()
V158()
V159()
V160()
V161()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) )
= {q2 : ( ( ) ( V43(2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below ) Element of NAT : ( ( ) ( V143() V144() V145() V146() V147() V148() V149() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V36() V143() V144() V145() V149() non bounded_below non bounded_above V209() ) set ) ) : ( ( ) ( ) set ) ) ) ) FinSequence-like V135() ) Point of ( ( ) ( non empty ) set ) ) } : ( ( ) ( non
empty )
set ) ;
theorem
for
P,
Q1 being ( ( non
empty ) ( non
empty )
Subset of )
for
p1,
p2,
q1,
q2 being ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) st
P : ( ( non
empty ) ( non
empty )
Subset of )
is_an_arc_of p1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) &
Q1 : ( ( non
empty ) ( non
empty )
Subset of )
is_an_arc_of q1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
q2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) &
LE q1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
q2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
P : ( ( non
empty ) ( non
empty )
Subset of ) ,
p1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) &
Q1 : ( ( non
empty ) ( non
empty )
Subset of )
c= P : ( ( non
empty ) ( non
empty )
Subset of ) holds
Q1 : ( ( non
empty ) ( non
empty )
Subset of )
= Segment (
P : ( ( non
empty ) ( non
empty )
Subset of ) ,
p1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
q1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
q2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( )
Element of
K6( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below ) Element of NAT : ( ( ) ( V143() V144() V145() V146() V147() V148() V149() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V36() V143() V144() V145() V149() non bounded_below non bounded_above V209() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like V109()
V155()
V156()
V157()
V158()
V159()
V160()
V161()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ) ;
theorem
for
P being ( ( non
empty ) ( non
empty )
Subset of )
for
p1,
p2,
q1,
q2,
p being ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
for
e being ( ( ) (
V11()
real ext-real )
Real) st
q1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
is_Lin P : ( ( non
empty ) ( non
empty )
Subset of ) ,
p1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
e : ( ( ) (
V11()
real ext-real )
Real) &
q2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) )
= e : ( ( ) (
V11()
real ext-real )
Real) &
LSeg (
q1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
q2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty V226(
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like V109()
V155()
V156()
V157()
V158()
V159()
V160()
V161()
strict )
RLTopStruct ) ) )
Element of
K6( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below ) Element of NAT : ( ( ) ( V143() V144() V145() V146() V147() V148() V149() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V36() V143() V144() V145() V149() non bounded_below non bounded_above V209() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like V109()
V155()
V156()
V157()
V158()
V159()
V160()
V161()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) )
c= P : ( ( non
empty ) ( non
empty )
Subset of ) &
p : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
in LSeg (
q1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
q2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty V226(
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like V109()
V155()
V156()
V157()
V158()
V159()
V160()
V161()
strict )
RLTopStruct ) ) )
Element of
K6( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below ) Element of NAT : ( ( ) ( V143() V144() V145() V146() V147() V148() V149() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V36() V143() V144() V145() V149() non bounded_below non bounded_above V209() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like V109()
V155()
V156()
V157()
V158()
V159()
V160()
V161()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ) holds
p : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
is_Lin P : ( ( non
empty ) ( non
empty )
Subset of ) ,
p1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
e : ( ( ) (
V11()
real ext-real )
Real) ;
theorem
for
P being ( ( non
empty ) ( non
empty )
Subset of )
for
p1,
p2,
q1,
q2,
p being ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
for
e being ( ( ) (
V11()
real ext-real )
Real) st
q1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
is_Rin P : ( ( non
empty ) ( non
empty )
Subset of ) ,
p1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
e : ( ( ) (
V11()
real ext-real )
Real) &
q2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) )
= e : ( ( ) (
V11()
real ext-real )
Real) &
LSeg (
q1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
q2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty V226(
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like V109()
V155()
V156()
V157()
V158()
V159()
V160()
V161()
strict )
RLTopStruct ) ) )
Element of
K6( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below ) Element of NAT : ( ( ) ( V143() V144() V145() V146() V147() V148() V149() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V36() V143() V144() V145() V149() non bounded_below non bounded_above V209() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like V109()
V155()
V156()
V157()
V158()
V159()
V160()
V161()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) )
c= P : ( ( non
empty ) ( non
empty )
Subset of ) &
p : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
in LSeg (
q1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
q2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty V226(
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like V109()
V155()
V156()
V157()
V158()
V159()
V160()
V161()
strict )
RLTopStruct ) ) )
Element of
K6( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below ) Element of NAT : ( ( ) ( V143() V144() V145() V146() V147() V148() V149() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V36() V143() V144() V145() V149() non bounded_below non bounded_above V209() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like V109()
V155()
V156()
V157()
V158()
V159()
V160()
V161()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ) holds
p : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
is_Rin P : ( ( non
empty ) ( non
empty )
Subset of ) ,
p1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
e : ( ( ) (
V11()
real ext-real )
Real) ;
theorem
for
P being ( ( non
empty ) ( non
empty )
Subset of )
for
p1,
p2,
q1,
q2,
p being ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
for
e being ( ( ) (
V11()
real ext-real )
Real) st
q1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
is_Lout P : ( ( non
empty ) ( non
empty )
Subset of ) ,
p1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
e : ( ( ) (
V11()
real ext-real )
Real) &
q2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) )
= e : ( ( ) (
V11()
real ext-real )
Real) &
LSeg (
q1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
q2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty V226(
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like V109()
V155()
V156()
V157()
V158()
V159()
V160()
V161()
strict )
RLTopStruct ) ) )
Element of
K6( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below ) Element of NAT : ( ( ) ( V143() V144() V145() V146() V147() V148() V149() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V36() V143() V144() V145() V149() non bounded_below non bounded_above V209() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like V109()
V155()
V156()
V157()
V158()
V159()
V160()
V161()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) )
c= P : ( ( non
empty ) ( non
empty )
Subset of ) &
p : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
in LSeg (
q1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
q2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty V226(
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like V109()
V155()
V156()
V157()
V158()
V159()
V160()
V161()
strict )
RLTopStruct ) ) )
Element of
K6( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below ) Element of NAT : ( ( ) ( V143() V144() V145() V146() V147() V148() V149() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V36() V143() V144() V145() V149() non bounded_below non bounded_above V209() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like V109()
V155()
V156()
V157()
V158()
V159()
V160()
V161()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ) holds
p : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
is_Lout P : ( ( non
empty ) ( non
empty )
Subset of ) ,
p1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
e : ( ( ) (
V11()
real ext-real )
Real) ;
theorem
for
P being ( ( non
empty ) ( non
empty )
Subset of )
for
p1,
p2,
q1,
q2,
p being ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
for
e being ( ( ) (
V11()
real ext-real )
Real) st
q1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
is_Rout P : ( ( non
empty ) ( non
empty )
Subset of ) ,
p1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
e : ( ( ) (
V11()
real ext-real )
Real) &
q2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
`1 : ( ( ) (
V11()
real ext-real )
Element of
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) )
= e : ( ( ) (
V11()
real ext-real )
Real) &
LSeg (
q1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
q2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty V226(
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like V109()
V155()
V156()
V157()
V158()
V159()
V160()
V161()
strict )
RLTopStruct ) ) )
Element of
K6( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below ) Element of NAT : ( ( ) ( V143() V144() V145() V146() V147() V148() V149() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V36() V143() V144() V145() V149() non bounded_below non bounded_above V209() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like V109()
V155()
V156()
V157()
V158()
V159()
V160()
V161()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) )
c= P : ( ( non
empty ) ( non
empty )
Subset of ) &
p : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
in LSeg (
q1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
q2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ) : ( ( ) ( non
empty V226(
TOP-REAL 2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) : ( (
strict ) ( non
empty TopSpace-like V109()
V155()
V156()
V157()
V158()
V159()
V160()
V161()
strict )
RLTopStruct ) ) )
Element of
K6( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty ordinal natural V11() real ext-real positive non negative V80() V81() V143() V144() V145() V146() V147() V148() left_end bounded_below ) Element of NAT : ( ( ) ( V143() V144() V145() V146() V147() V148() V149() bounded_below ) Element of K6(REAL : ( ( ) ( non empty V36() V143() V144() V145() V149() non bounded_below non bounded_above V209() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like V109()
V155()
V156()
V157()
V158()
V159()
V160()
V161()
strict )
RLTopStruct ) : ( ( ) ( non
empty )
set ) ) : ( ( ) ( )
set ) ) holds
p : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) )
is_Rout P : ( ( non
empty ) ( non
empty )
Subset of ) ,
p1 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
p2 : ( ( ) (
V43(2 : ( ( ) ( non
empty ordinal natural V11()
real ext-real positive non
negative V80()
V81()
V143()
V144()
V145()
V146()
V147()
V148()
left_end bounded_below )
Element of
NAT : ( ( ) (
V143()
V144()
V145()
V146()
V147()
V148()
V149()
bounded_below )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V143()
V144()
V145()
V149() non
bounded_below non
bounded_above V209() )
set ) ) : ( ( ) ( )
set ) ) ) )
FinSequence-like V135() )
Point of ( ( ) ( non
empty )
set ) ) ,
e : ( ( ) (
V11()
real ext-real )
Real) ;