begin
theorem
for
P being ( ( ) ( )
Subset of ( ( ) ( )
set ) )
for
p1,
p2,
q1,
q2 being ( ( ) (
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real V100()
V101()
V148()
V149()
V150()
V151()
V152()
V153() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154() )
set ) ) : ( ( ) ( )
set ) ) ) )
V97()
V140() )
Point of ( ( ) ( non
empty V30() )
set ) ) st
P : ( ( ) ( )
Subset of ( ( ) ( )
set ) )
is_an_arc_of p1 : ( ( ) (
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real V100()
V101()
V148()
V149()
V150()
V151()
V152()
V153() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154() )
set ) ) : ( ( ) ( )
set ) ) ) )
V97()
V140() )
Point of ( ( ) ( non
empty V30() )
set ) ) ,
p2 : ( ( ) (
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real V100()
V101()
V148()
V149()
V150()
V151()
V152()
V153() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154() )
set ) ) : ( ( ) ( )
set ) ) ) )
V97()
V140() )
Point of ( ( ) ( non
empty V30() )
set ) ) &
p1 : ( ( ) (
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real V100()
V101()
V148()
V149()
V150()
V151()
V152()
V153() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154() )
set ) ) : ( ( ) ( )
set ) ) ) )
V97()
V140() )
Point of ( ( ) ( non
empty V30() )
set ) )
<> q1 : ( ( ) (
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real V100()
V101()
V148()
V149()
V150()
V151()
V152()
V153() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154() )
set ) ) : ( ( ) ( )
set ) ) ) )
V97()
V140() )
Point of ( ( ) ( non
empty V30() )
set ) ) &
p2 : ( ( ) (
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real V100()
V101()
V148()
V149()
V150()
V151()
V152()
V153() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154() )
set ) ) : ( ( ) ( )
set ) ) ) )
V97()
V140() )
Point of ( ( ) ( non
empty V30() )
set ) )
<> q2 : ( ( ) (
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real V100()
V101()
V148()
V149()
V150()
V151()
V152()
V153() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154() )
set ) ) : ( ( ) ( )
set ) ) ) )
V97()
V140() )
Point of ( ( ) ( non
empty V30() )
set ) ) holds
( not
p1 : ( ( ) (
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real V100()
V101()
V148()
V149()
V150()
V151()
V152()
V153() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154() )
set ) ) : ( ( ) ( )
set ) ) ) )
V97()
V140() )
Point of ( ( ) ( non
empty V30() )
set ) )
in Segment (
P : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ,
p1 : ( ( ) (
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real V100()
V101()
V148()
V149()
V150()
V151()
V152()
V153() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154() )
set ) ) : ( ( ) ( )
set ) ) ) )
V97()
V140() )
Point of ( ( ) ( non
empty V30() )
set ) ) ,
p2 : ( ( ) (
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real V100()
V101()
V148()
V149()
V150()
V151()
V152()
V153() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154() )
set ) ) : ( ( ) ( )
set ) ) ) )
V97()
V140() )
Point of ( ( ) ( non
empty V30() )
set ) ) ,
q1 : ( ( ) (
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real V100()
V101()
V148()
V149()
V150()
V151()
V152()
V153() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154() )
set ) ) : ( ( ) ( )
set ) ) ) )
V97()
V140() )
Point of ( ( ) ( non
empty V30() )
set ) ) ,
q2 : ( ( ) (
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real V100()
V101()
V148()
V149()
V150()
V151()
V152()
V153() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154() )
set ) ) : ( ( ) ( )
set ) ) ) )
V97()
V140() )
Point of ( ( ) ( non
empty V30() )
set ) ) ) : ( ( ) ( )
Element of
K6( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_2 V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict add-continuous Mult-continuous )
RLTopStruct ) : ( ( ) ( non
empty V30() )
set ) ) : ( ( ) ( )
set ) ) & not
p2 : ( ( ) (
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real V100()
V101()
V148()
V149()
V150()
V151()
V152()
V153() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154() )
set ) ) : ( ( ) ( )
set ) ) ) )
V97()
V140() )
Point of ( ( ) ( non
empty V30() )
set ) )
in Segment (
P : ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ,
p1 : ( ( ) (
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real V100()
V101()
V148()
V149()
V150()
V151()
V152()
V153() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154() )
set ) ) : ( ( ) ( )
set ) ) ) )
V97()
V140() )
Point of ( ( ) ( non
empty V30() )
set ) ) ,
p2 : ( ( ) (
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real V100()
V101()
V148()
V149()
V150()
V151()
V152()
V153() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154() )
set ) ) : ( ( ) ( )
set ) ) ) )
V97()
V140() )
Point of ( ( ) ( non
empty V30() )
set ) ) ,
q1 : ( ( ) (
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real V100()
V101()
V148()
V149()
V150()
V151()
V152()
V153() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154() )
set ) ) : ( ( ) ( )
set ) ) ) )
V97()
V140() )
Point of ( ( ) ( non
empty V30() )
set ) ) ,
q2 : ( ( ) (
V43(2 : ( ( ) ( non
empty natural V11()
real ext-real V100()
V101()
V148()
V149()
V150()
V151()
V152()
V153() )
Element of
NAT : ( ( ) (
V148()
V149()
V150()
V151()
V152()
V153()
V154() )
Element of
K6(
REAL : ( ( ) ( non
empty V36()
V148()
V149()
V150()
V154() )
set ) ) : ( ( ) ( )
set ) ) ) )
V97()
V140() )
Point of ( ( ) ( non
empty V30() )
set ) ) ) : ( ( ) ( )
Element of
K6( the
carrier of
(TOP-REAL 2 : ( ( ) ( non empty natural V11() real ext-real V100() V101() V148() V149() V150() V151() V152() V153() ) Element of NAT : ( ( ) ( V148() V149() V150() V151() V152() V153() V154() ) Element of K6(REAL : ( ( ) ( non empty V36() V148() V149() V150() V154() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( (
strict ) ( non
empty TopSpace-like T_2 V114()
V160()
V161()
V162()
V163()
V164()
V165()
V166()
strict add-continuous Mult-continuous )
RLTopStruct ) : ( ( ) ( non
empty V30() )
set ) ) : ( ( ) ( )
set ) ) ) ;
definition
let D be ( ( ) ( )
Subset of ) ;
end;
begin
begin
begin
definition
let P be ( ( ) ( )
Subset of ( ( ) ( )
set ) ) ;
end;