:: Graph Theoretical Properties of Arcs in the Plane and Fashoda Meet Theorem
:: by Yatsuka Nakamura
::
:: Received August 21, 1998
:: Copyright (c) 1998-2012 Association of Mizar Users
begin
theorem
Th1
:
:: JGRAPH_1:1
for
G
being
Graph
for
IT
being
oriented
Chain
of
G
for
vs
being
FinSequence
of the
carrier
of
G
st
IT
is
Simple
&
vs
is_oriented_vertex_seq_of
IT
holds
for
n
,
m
being
Element
of
NAT
st 1
<=
n
&
n
<
m
&
m
<=
len
vs
&
vs
.
n
=
vs
.
m
holds
(
n
=
1 &
m
=
len
vs
)
proof
end;
definition
let
X
be
set
;
func
PGraph
X
->
MultiGraphStruct
equals
:: JGRAPH_1:def 1
MultiGraphStruct
(#
X
,
[:
X
,
X
:]
,
(
pr1
(
X
,
X
)
)
,
(
pr2
(
X
,
X
)
)
#);
coherence
MultiGraphStruct
(#
X
,
[:
X
,
X
:]
,
(
pr1
(
X
,
X
)
)
,
(
pr2
(
X
,
X
)
)
#) is
MultiGraphStruct
;
end;
::
deftheorem
defines
PGraph
JGRAPH_1:def 1 :
for
X
being
set
holds
PGraph
X
=
MultiGraphStruct
(#
X
,
[:
X
,
X
:]
,
(
pr1
(
X
,
X
)
)
,
(
pr2
(
X
,
X
)
)
#);
theorem
:: JGRAPH_1:2
for
X
being
set
holds the
carrier
of
(
PGraph
X
)
=
X
;
definition
let
f
be
FinSequence
;
func
PairF
f
->
FinSequence
means
:
Def2
:
:: JGRAPH_1:def 2
(
len
it
=
(
len
f
)
-'
1 & ( for
i
being
Element
of
NAT
st 1
<=
i
&
i
<
len
f
holds
it
.
i
=
[
(
f
.
i
)
,
(
f
.
(
i
+
1
)
)
]
) );
existence
ex
b
1
being
FinSequence
st
(
len
b
1
=
(
len
f
)
-'
1 & ( for
i
being
Element
of
NAT
st 1
<=
i
&
i
<
len
f
holds
b
1
.
i
=
[
(
f
.
i
)
,
(
f
.
(
i
+
1
)
)
]
) )
proof
end;
uniqueness
for
b
1
,
b
2
being
FinSequence
st
len
b
1
=
(
len
f
)
-'
1 & ( for
i
being
Element
of
NAT
st 1
<=
i
&
i
<
len
f
holds
b
1
.
i
=
[
(
f
.
i
)
,
(
f
.
(
i
+
1
)
)
]
) &
len
b
2
=
(
len
f
)
-'
1 & ( for
i
being
Element
of
NAT
st 1
<=
i
&
i
<
len
f
holds
b
2
.
i
=
[
(
f
.
i
)
,
(
f
.
(
i
+
1
)
)
]
) holds
b
1
=
b
2
proof
end;
end;
::
deftheorem
Def2
defines
PairF
JGRAPH_1:def 2 :
for
f
,
b
2
being
FinSequence
holds
(
b
2
=
PairF
f
iff (
len
b
2
=
(
len
f
)
-'
1 & ( for
i
being
Element
of
NAT
st 1
<=
i
&
i
<
len
f
holds
b
2
.
i
=
[
(
f
.
i
)
,
(
f
.
(
i
+
1
)
)
]
) ) );
registration
let
X
be non
empty
set
;
cluster
PGraph
X
->
non
empty
;
coherence
not
PGraph
X
is
empty
;
end;
theorem
:: JGRAPH_1:3
for
X
being non
empty
set
for
f
being
FinSequence
of
X
holds
f
is
FinSequence
of the
carrier
of
(
PGraph
X
)
;
theorem
Th4
:
:: JGRAPH_1:4
for
X
being non
empty
set
for
f
being
FinSequence
of
X
holds
PairF
f
is
FinSequence
of the
carrier'
of
(
PGraph
X
)
proof
end;
definition
let
X
be non
empty
set
;
let
f
be
FinSequence
of
X
;
:: original:
PairF
redefine
func
PairF
f
->
FinSequence
of the
carrier'
of
(
PGraph
X
)
;
coherence
PairF
f
is
FinSequence
of the
carrier'
of
(
PGraph
X
)
by
Th4
;
end;
theorem
Th5
:
:: JGRAPH_1:5
for
X
being non
empty
set
for
n
being
Element
of
NAT
for
f
being
FinSequence
of
X
st 1
<=
n
&
n
<=
len
(
PairF
f
)
holds
(
PairF
f
)
.
n
in
the
carrier'
of
(
PGraph
X
)
proof
end;
theorem
Th6
:
:: JGRAPH_1:6
for
X
being non
empty
set
for
f
being
FinSequence
of
X
holds
PairF
f
is
oriented
Chain
of
PGraph
X
proof
end;
definition
let
X
be non
empty
set
;
let
f
be
FinSequence
of
X
;
:: original:
PairF
redefine
func
PairF
f
->
oriented
Chain
of
PGraph
X
;
coherence
PairF
f
is
oriented
Chain
of
PGraph
X
by
Th6
;
end;
theorem
Th7
:
:: JGRAPH_1:7
for
X
being non
empty
set
for
f
being
FinSequence
of
X
for
f1
being
FinSequence
of the
carrier
of
(
PGraph
X
)
st
len
f
>=
1 &
f
=
f1
holds
f1
is_oriented_vertex_seq_of
PairF
f
proof
end;
begin
definition
let
X
be non
empty
set
;
let
f
,
g
be
FinSequence
of
X
;
pred
g
is_Shortcut_of
f
means
:
Def3
:
:: JGRAPH_1:def 3
(
f
.
1
=
g
.
1 &
f
.
(
len
f
)
=
g
.
(
len
g
)
& ex
fc
being
Subset
of
(
PairF
f
)
ex
fvs
being
Subset
of
f
ex
sc
being
oriented
simple
Chain
of
PGraph
X
ex
g1
being
FinSequence
of the
carrier
of
(
PGraph
X
)
st
(
Seq
fc
=
sc
&
Seq
fvs
=
g
&
g1
=
g
&
g1
is_oriented_vertex_seq_of
sc
) );
end;
::
deftheorem
Def3
defines
is_Shortcut_of
JGRAPH_1:def 3 :
for
X
being non
empty
set
for
f
,
g
being
FinSequence
of
X
holds
(
g
is_Shortcut_of
f
iff (
f
.
1
=
g
.
1 &
f
.
(
len
f
)
=
g
.
(
len
g
)
& ex
fc
being
Subset
of
(
PairF
f
)
ex
fvs
being
Subset
of
f
ex
sc
being
oriented
simple
Chain
of
PGraph
X
ex
g1
being
FinSequence
of the
carrier
of
(
PGraph
X
)
st
(
Seq
fc
=
sc
&
Seq
fvs
=
g
&
g1
=
g
&
g1
is_oriented_vertex_seq_of
sc
) ) );
theorem
Th8
:
:: JGRAPH_1:8
for
X
being non
empty
set
for
f
,
g
being
FinSequence
of
X
st
g
is_Shortcut_of
f
holds
( 1
<=
len
g
&
len
g
<=
len
f
)
proof
end;
theorem
Th9
:
:: JGRAPH_1:9
for
X
being non
empty
set
for
f
being
FinSequence
of
X
st
len
f
>=
1 holds
ex
g
being
FinSequence
of
X
st
g
is_Shortcut_of
f
proof
end;
theorem
Th10
:
:: JGRAPH_1:10
for
X
being non
empty
set
for
f
,
g
being
FinSequence
of
X
st
g
is_Shortcut_of
f
holds
rng
(
PairF
g
)
c=
rng
(
PairF
f
)
proof
end;
theorem
Th11
:
:: JGRAPH_1:11
for
X
being non
empty
set
for
f
,
g
being
FinSequence
of
X
st
f
.
1
<>
f
.
(
len
f
)
&
g
is_Shortcut_of
f
holds
g
is
one-to-one
proof
end;
definition
let
n
be
Element
of
NAT
;
let
IT
be
FinSequence
of
(
TOP-REAL
n
)
;
attr
IT
is
nodic
means
:
Def4
:
:: JGRAPH_1:def 4
for
i
,
j
being
Element
of
NAT
holds
( not
LSeg
(
IT
,
i
)
meets
LSeg
(
IT
,
j
) or (
(
LSeg
(
IT
,
i
)
)
/\
(
LSeg
(
IT
,
j
)
)
=
{
(
IT
.
i
)
}
& (
IT
.
i
=
IT
.
j
or
IT
.
i
=
IT
.
(
j
+
1
)
) ) or (
(
LSeg
(
IT
,
i
)
)
/\
(
LSeg
(
IT
,
j
)
)
=
{
(
IT
.
(
i
+
1
)
)
}
& (
IT
.
(
i
+
1
)
=
IT
.
j
or
IT
.
(
i
+
1
)
=
IT
.
(
j
+
1
)
) ) or
LSeg
(
IT
,
i
)
=
LSeg
(
IT
,
j
) );
end;
::
deftheorem
Def4
defines
nodic
JGRAPH_1:def 4 :
for
n
being
Element
of
NAT
for
IT
being
FinSequence
of
(
TOP-REAL
n
)
holds
(
IT
is
nodic
iff for
i
,
j
being
Element
of
NAT
holds
( not
LSeg
(
IT
,
i
)
meets
LSeg
(
IT
,
j
) or (
(
LSeg
(
IT
,
i
)
)
/\
(
LSeg
(
IT
,
j
)
)
=
{
(
IT
.
i
)
}
& (
IT
.
i
=
IT
.
j
or
IT
.
i
=
IT
.
(
j
+
1
)
) ) or (
(
LSeg
(
IT
,
i
)
)
/\
(
LSeg
(
IT
,
j
)
)
=
{
(
IT
.
(
i
+
1
)
)
}
& (
IT
.
(
i
+
1
)
=
IT
.
j
or
IT
.
(
i
+
1
)
=
IT
.
(
j
+
1
)
) ) or
LSeg
(
IT
,
i
)
=
LSeg
(
IT
,
j
) ) );
theorem
:: JGRAPH_1:12
for
f
being
FinSequence
of
(
TOP-REAL
2
)
st
f
is
s.n.c.
holds
f
is
s.c.c.
proof
end;
theorem
Th13
:
:: JGRAPH_1:13
for
f
being
FinSequence
of
(
TOP-REAL
2
)
st
f
is
s.c.c.
&
LSeg
(
f
,1)
misses
LSeg
(
f
,
(
(
len
f
)
-'
1
)
) holds
f
is
s.n.c.
proof
end;
theorem
Th14
:
:: JGRAPH_1:14
for
f
being
FinSequence
of
(
TOP-REAL
2
)
st
f
is
nodic
&
PairF
f
is
Simple
holds
f
is
s.c.c.
proof
end;
theorem
Th15
:
:: JGRAPH_1:15
for
f
being
FinSequence
of
(
TOP-REAL
2
)
st
f
is
nodic
&
PairF
f
is
Simple
&
f
.
1
<>
f
.
(
len
f
)
holds
f
is
s.n.c.
proof
end;
theorem
Th16
:
:: JGRAPH_1:16
for
n
being
Element
of
NAT
for
p1
,
p2
,
p3
being
Point
of
(
TOP-REAL
n
)
holds
( for
x
being
set
holds
( not
x
<>
p2
or not
x
in
(
LSeg
(
p1
,
p2
)
)
/\
(
LSeg
(
p2
,
p3
)
)
) or
p1
in
LSeg
(
p2
,
p3
) or
p3
in
LSeg
(
p1
,
p2
) )
proof
end;
theorem
Th17
:
:: JGRAPH_1:17
for
f
being
FinSequence
of
(
TOP-REAL
2
)
st
f
is
s.n.c.
&
(
LSeg
(
f
,1)
)
/\
(
LSeg
(
f
,
(
1
+
1
)
)
)
c=
{
(
f
/.
(
1
+
1
)
)
}
&
(
LSeg
(
f
,
(
(
len
f
)
-'
2
)
)
)
/\
(
LSeg
(
f
,
(
(
len
f
)
-'
1
)
)
)
c=
{
(
f
/.
(
(
len
f
)
-'
1
)
)
}
holds
f
is
unfolded
proof
end;
theorem
Th18
:
:: JGRAPH_1:18
for
X
being non
empty
set
for
f
being
FinSequence
of
X
st
PairF
f
is
Simple
&
f
.
1
<>
f
.
(
len
f
)
holds
(
f
is
one-to-one
&
len
f
<>
1 )
proof
end;
theorem
:: JGRAPH_1:19
for
X
being non
empty
set
for
f
being
FinSequence
of
X
st
f
is
one-to-one
&
len
f
>
1 holds
(
PairF
f
is
Simple
&
f
.
1
<>
f
.
(
len
f
)
)
proof
end;
theorem
:: JGRAPH_1:20
for
f
being
FinSequence
of
(
TOP-REAL
2
)
st
f
is
nodic
&
PairF
f
is
Simple
&
f
.
1
<>
f
.
(
len
f
)
holds
f
is
unfolded
proof
end;
theorem
Th21
:
:: JGRAPH_1:21
for
f
,
g
being
FinSequence
of
(
TOP-REAL
2
)
for
i
being
Element
of
NAT
st
g
is_Shortcut_of
f
& 1
<=
i
&
i
+
1
<=
len
g
holds
ex
k1
being
Element
of
NAT
st
( 1
<=
k1
&
k1
+
1
<=
len
f
&
f
/.
k1
=
g
/.
i
&
f
/.
(
k1
+
1
)
=
g
/.
(
i
+
1
)
&
f
.
k1
=
g
.
i
&
f
.
(
k1
+
1
)
=
g
.
(
i
+
1
)
)
proof
end;
theorem
Th22
:
:: JGRAPH_1:22
for
f
,
g
being
FinSequence
of
(
TOP-REAL
2
)
st
g
is_Shortcut_of
f
holds
rng
g
c=
rng
f
proof
end;
theorem
Th23
:
:: JGRAPH_1:23
for
f
,
g
being
FinSequence
of
(
TOP-REAL
2
)
st
g
is_Shortcut_of
f
holds
L~
g
c=
L~
f
proof
end;
theorem
Th24
:
:: JGRAPH_1:24
for
f
,
g
being
FinSequence
of
(
TOP-REAL
2
)
st
f
is
special
&
g
is_Shortcut_of
f
holds
g
is
special
proof
end;
theorem
Th25
:
:: JGRAPH_1:25
for
f
being
FinSequence
of
(
TOP-REAL
2
)
st
f
is
special
& 2
<=
len
f
&
f
.
1
<>
f
.
(
len
f
)
holds
ex
g
being
FinSequence
of
(
TOP-REAL
2
)
st
( 2
<=
len
g
&
g
is
special
&
g
is
one-to-one
&
L~
g
c=
L~
f
&
f
.
1
=
g
.
1 &
f
.
(
len
f
)
=
g
.
(
len
g
)
&
rng
g
c=
rng
f
)
proof
end;
:: Goboard Theorem for general special sequences
theorem
Th26
:
:: JGRAPH_1:26
for
f1
,
f2
being
FinSequence
of
(
TOP-REAL
2
)
st
f1
is
special
&
f2
is
special
& 2
<=
len
f1
& 2
<=
len
f2
&
f1
.
1
<>
f1
.
(
len
f1
)
&
f2
.
1
<>
f2
.
(
len
f2
)
&
X_axis
f1
lies_between
(
X_axis
f1
)
.
1,
(
X_axis
f1
)
.
(
len
f1
)
&
X_axis
f2
lies_between
(
X_axis
f1
)
.
1,
(
X_axis
f1
)
.
(
len
f1
)
&
Y_axis
f1
lies_between
(
Y_axis
f2
)
.
1,
(
Y_axis
f2
)
.
(
len
f2
)
&
Y_axis
f2
lies_between
(
Y_axis
f2
)
.
1,
(
Y_axis
f2
)
.
(
len
f2
)
holds
L~
f1
meets
L~
f2
proof
end;
begin
theorem
Th27
:
:: JGRAPH_1:27
for
a
,
b
,
r1
,
r2
being
Real
st
a
<=
r1
&
r1
<=
b
&
a
<=
r2
&
r2
<=
b
holds
abs
(
r1
-
r2
)
<=
b
-
a
proof
end;
theorem
Th28
:
:: JGRAPH_1:28
for
n
being
Element
of
NAT
for
p1
,
p2
being
Point
of
(
TOP-REAL
n
)
for
x1
,
x2
being
Point
of
(
Euclid
n
)
st
x1
=
p1
&
x2
=
p2
holds
|.
(
p1
-
p2
)
.|
=
dist
(
x1
,
x2
)
proof
end;
theorem
Th29
:
:: JGRAPH_1:29
for
p
being
Point
of
(
TOP-REAL
2
)
holds
|.
p
.|
^2
=
(
(
p
`1
)
^2
)
+
(
(
p
`2
)
^2
)
proof
end;
theorem
Th30
:
:: JGRAPH_1:30
for
p
being
Point
of
(
TOP-REAL
2
)
holds
|.
p
.|
=
sqrt
(
(
(
p
`1
)
^2
)
+
(
(
p
`2
)
^2
)
)
proof
end;
theorem
Th31
:
:: JGRAPH_1:31
for
p
being
Point
of
(
TOP-REAL
2
)
holds
|.
p
.|
<=
(
abs
(
p
`1
)
)
+
(
abs
(
p
`2
)
)
proof
end;
theorem
Th32
:
:: JGRAPH_1:32
for
p1
,
p2
being
Point
of
(
TOP-REAL
2
)
holds
|.
(
p1
-
p2
)
.|
<=
(
abs
(
(
p1
`1
)
-
(
p2
`1
)
)
)
+
(
abs
(
(
p1
`2
)
-
(
p2
`2
)
)
)
proof
end;
theorem
Th33
:
:: JGRAPH_1:33
for
p
being
Point
of
(
TOP-REAL
2
)
holds
(
abs
(
p
`1
)
<=
|.
p
.|
&
abs
(
p
`2
)
<=
|.
p
.|
)
proof
end;
theorem
Th34
:
:: JGRAPH_1:34
for
p1
,
p2
being
Point
of
(
TOP-REAL
2
)
holds
(
abs
(
(
p1
`1
)
-
(
p2
`1
)
)
<=
|.
(
p1
-
p2
)
.|
&
abs
(
(
p1
`2
)
-
(
p2
`2
)
)
<=
|.
(
p1
-
p2
)
.|
)
proof
end;
theorem
Th35
:
:: JGRAPH_1:35
for
n
being
Element
of
NAT
for
p
,
p1
,
p2
being
Point
of
(
TOP-REAL
n
)
st
p
in
LSeg
(
p1
,
p2
) holds
ex
r
being
Real
st
(
0
<=
r
&
r
<=
1 &
p
=
(
(
1
-
r
)
*
p1
)
+
(
r
*
p2
)
)
proof
end;
theorem
Th36
:
:: JGRAPH_1:36
for
n
being
Element
of
NAT
for
p
,
p1
,
p2
being
Point
of
(
TOP-REAL
n
)
st
p
in
LSeg
(
p1
,
p2
) holds
(
|.
(
p
-
p1
)
.|
<=
|.
(
p1
-
p2
)
.|
&
|.
(
p
-
p2
)
.|
<=
|.
(
p1
-
p2
)
.|
)
proof
end;
begin
theorem
Th37
:
:: JGRAPH_1:37
for
M
being non
empty
MetrSpace
for
P
,
Q
being
Subset
of
(
TopSpaceMetr
M
)
st
P
<>
{}
&
P
is
compact
&
Q
<>
{}
&
Q
is
compact
holds
min_dist_min
(
P
,
Q
)
>=
0
proof
end;
theorem
Th38
:
:: JGRAPH_1:38
for
M
being non
empty
MetrSpace
for
P
,
Q
being
Subset
of
(
TopSpaceMetr
M
)
st
P
<>
{}
&
P
is
compact
&
Q
<>
{}
&
Q
is
compact
holds
(
P
misses
Q
iff
min_dist_min
(
P
,
Q
)
>
0
)
proof
end;
:: Approximation of finite sequence by special finite sequence
theorem
Th39
:
:: JGRAPH_1:39
for
f
being
FinSequence
of
(
TOP-REAL
2
)
for
a
,
c
,
d
being
Real
st 1
<=
len
f
&
X_axis
f
lies_between
(
X_axis
f
)
.
1,
(
X_axis
f
)
.
(
len
f
)
&
Y_axis
f
lies_between
c
,
d
&
a
>
0
& ( for
i
being
Element
of
NAT
st 1
<=
i
&
i
+
1
<=
len
f
holds
|.
(
(
f
/.
i
)
-
(
f
/.
(
i
+
1
)
)
)
.|
<
a
) holds
ex
g
being
FinSequence
of
(
TOP-REAL
2
)
st
(
g
is
special
&
g
.
1
=
f
.
1 &
g
.
(
len
g
)
=
f
.
(
len
f
)
&
len
g
>=
len
f
&
X_axis
g
lies_between
(
X_axis
f
)
.
1,
(
X_axis
f
)
.
(
len
f
)
&
Y_axis
g
lies_between
c
,
d
& ( for
j
being
Element
of
NAT
st
j
in
dom
g
holds
ex
k
being
Element
of
NAT
st
(
k
in
dom
f
&
|.
(
(
g
/.
j
)
-
(
f
/.
k
)
)
.|
<
a
) ) & ( for
j
being
Element
of
NAT
st 1
<=
j
&
j
+
1
<=
len
g
holds
|.
(
(
g
/.
j
)
-
(
g
/.
(
j
+
1
)
)
)
.|
<
a
) )
proof
end;
theorem
Th40
:
:: JGRAPH_1:40
for
f
being
FinSequence
of
(
TOP-REAL
2
)
for
a
,
c
,
d
being
Real
st 1
<=
len
f
&
Y_axis
f
lies_between
(
Y_axis
f
)
.
1,
(
Y_axis
f
)
.
(
len
f
)
&
X_axis
f
lies_between
c
,
d
&
a
>
0
& ( for
i
being
Element
of
NAT
st 1
<=
i
&
i
+
1
<=
len
f
holds
|.
(
(
f
/.
i
)
-
(
f
/.
(
i
+
1
)
)
)
.|
<
a
) holds
ex
g
being
FinSequence
of
(
TOP-REAL
2
)
st
(
g
is
special
&
g
.
1
=
f
.
1 &
g
.
(
len
g
)
=
f
.
(
len
f
)
&
len
g
>=
len
f
&
Y_axis
g
lies_between
(
Y_axis
f
)
.
1,
(
Y_axis
f
)
.
(
len
f
)
&
X_axis
g
lies_between
c
,
d
& ( for
j
being
Element
of
NAT
st
j
in
dom
g
holds
ex
k
being
Element
of
NAT
st
(
k
in
dom
f
&
|.
(
(
g
/.
j
)
-
(
f
/.
k
)
)
.|
<
a
) ) & ( for
j
being
Element
of
NAT
st 1
<=
j
&
j
+
1
<=
len
g
holds
|.
(
(
g
/.
j
)
-
(
g
/.
(
j
+
1
)
)
)
.|
<
a
) )
proof
end;
theorem
Th41
:
:: JGRAPH_1:41
for
f
being
FinSequence
of
(
TOP-REAL
2
)
st 1
<=
len
f
holds
(
len
(
X_axis
f
)
=
len
f
&
(
X_axis
f
)
.
1
=
(
f
/.
1
)
`1
&
(
X_axis
f
)
.
(
len
f
)
=
(
f
/.
(
len
f
)
)
`1
)
proof
end;
theorem
Th42
:
:: JGRAPH_1:42
for
f
being
FinSequence
of
(
TOP-REAL
2
)
st 1
<=
len
f
holds
(
len
(
Y_axis
f
)
=
len
f
&
(
Y_axis
f
)
.
1
=
(
f
/.
1
)
`2
&
(
Y_axis
f
)
.
(
len
f
)
=
(
f
/.
(
len
f
)
)
`2
)
proof
end;
theorem
Th43
:
:: JGRAPH_1:43
for
i
being
Element
of
NAT
for
f
being
FinSequence
of
(
TOP-REAL
2
)
st
i
in
dom
f
holds
(
(
X_axis
f
)
.
i
=
(
f
/.
i
)
`1
&
(
Y_axis
f
)
.
i
=
(
f
/.
i
)
`2
)
proof
end;
:: Goboard Theorem in continuous case
theorem
Th44
:
:: JGRAPH_1:44
for
P
,
Q
being non
empty
Subset
of
(
TOP-REAL
2
)
for
p1
,
p2
,
q1
,
q2
being
Point
of
(
TOP-REAL
2
)
st
P
is_an_arc_of
p1
,
p2
&
Q
is_an_arc_of
q1
,
q2
& ( for
p
being
Point
of
(
TOP-REAL
2
)
st
p
in
P
holds
(
p1
`1
<=
p
`1
&
p
`1
<=
p2
`1
) ) & ( for
p
being
Point
of
(
TOP-REAL
2
)
st
p
in
Q
holds
(
p1
`1
<=
p
`1
&
p
`1
<=
p2
`1
) ) & ( for
p
being
Point
of
(
TOP-REAL
2
)
st
p
in
P
holds
(
q1
`2
<=
p
`2
&
p
`2
<=
q2
`2
) ) & ( for
p
being
Point
of
(
TOP-REAL
2
)
st
p
in
Q
holds
(
q1
`2
<=
p
`2
&
p
`2
<=
q2
`2
) ) holds
P
meets
Q
proof
end;
theorem
Th45
:
:: JGRAPH_1:45
for
X
,
Y
being non
empty
TopSpace
for
f
being
Function
of
X
,
Y
for
P
being non
empty
Subset
of
Y
for
f1
being
Function
of
X
,
(
Y
|
P
)
st
f
=
f1
&
f
is
continuous
holds
f1
is
continuous
proof
end;
theorem
Th46
:
:: JGRAPH_1:46
for
X
,
Y
being non
empty
TopSpace
for
f
being
Function
of
X
,
Y
for
P
being non
empty
Subset
of
Y
st
X
is
compact
&
Y
is
T_2
&
f
is
continuous
&
f
is
one-to-one
&
P
=
rng
f
holds
ex
f1
being
Function
of
X
,
(
Y
|
P
)
st
(
f
=
f1
&
f1
is
being_homeomorphism
)
proof
end;
::
Fashoda Meet Theorem
theorem
:: JGRAPH_1:47
for
f
,
g
being
Function
of
I[01]
,
(
TOP-REAL
2
)
for
a
,
b
,
c
,
d
being
real
number
for
O
,
I
being
Point
of
I[01]
st
O
=
0
&
I
=
1 &
f
is
continuous
&
f
is
one-to-one
&
g
is
continuous
&
g
is
one-to-one
&
(
f
.
O
)
`1
=
a
&
(
f
.
I
)
`1
=
b
&
(
g
.
O
)
`2
=
c
&
(
g
.
I
)
`2
=
d
& ( for
r
being
Point
of
I[01]
holds
(
a
<=
(
f
.
r
)
`1
&
(
f
.
r
)
`1
<=
b
&
a
<=
(
g
.
r
)
`1
&
(
g
.
r
)
`1
<=
b
&
c
<=
(
f
.
r
)
`2
&
(
f
.
r
)
`2
<=
d
&
c
<=
(
g
.
r
)
`2
&
(
g
.
r
)
`2
<=
d
) ) holds
rng
f
meets
rng
g
proof
end;