:: JGRAPH_6 semantic presentation
:: Showing IDV graph ... (Click the Palm Trees again to close it)
theorem :: JGRAPH_6:1
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem Th2: :: JGRAPH_6:2
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
Lm1:
for a, b being real number st ( ( a >= 0 & b > 0 ) or ( a > 0 & b >= 0 ) ) holds
a + b > 0
by XREAL_1:36;
theorem :: JGRAPH_6:3
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem Th4: :: JGRAPH_6:4
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th5: :: JGRAPH_6:5
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
Lm2:
for a, b being real number st - 1 <= a & a <= 1 & - 1 <= b & b <= 1 holds
(1 + (a ^2 )) * (b ^2 ) <= 1 + (b ^2 )
theorem Th6: :: JGRAPH_6:6
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th7: :: JGRAPH_6:7
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
Lm3:
for a, b being real number st b <= 0 & a <= b holds
a * (sqrt (1 + (b ^2 ))) <= b * (sqrt (1 + (a ^2 )))
Lm4:
for a, b being real number st a <= 0 & a <= b holds
a * (sqrt (1 + (b ^2 ))) <= b * (sqrt (1 + (a ^2 )))
Lm5:
for a, b being real number st a >= 0 & a >= b holds
a * (sqrt (1 + (b ^2 ))) >= b * (sqrt (1 + (a ^2 )))
theorem Th8: :: JGRAPH_6:8
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th9: :: JGRAPH_6:9
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th10: :: JGRAPH_6:10
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th11: :: JGRAPH_6:11
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th12: :: JGRAPH_6:12
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th13: :: JGRAPH_6:13
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th14: :: JGRAPH_6:14
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th15: :: JGRAPH_6:15
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th16: :: JGRAPH_6:16
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th17: :: JGRAPH_6:17
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th18: :: JGRAPH_6:18
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: JGRAPH_6:19
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th20: :: JGRAPH_6:20
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th21: :: JGRAPH_6:21
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th22: :: JGRAPH_6:22
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
Lm6:
( |[(- 1),0]| `1 = - 1 & |[(- 1),0]| `2 = 0 & |[1,0]| `1 = 1 & |[1,0]| `2 = 0 & |[0,(- 1)]| `1 = 0 & |[0,(- 1)]| `2 = - 1 & |[0,1]| `1 = 0 & |[0,1]| `2 = 1 )
by EUCLID:56;
Lm7:
now
thus |.|[(- 1),0]|.| =
sqrt (((- 1) ^2 ) + (0 ^2 ))
by Lm6, JGRAPH_3:10
.=
1
by SQUARE_1:59, SQUARE_1:60, SQUARE_1:61, SQUARE_1:83
;
:: thesis: ( |.|[1,0]|.| = 1 & |.|[0,(- 1)]|.| = 1 & |.|[0,1]|.| = 1 )thus |.|[1,0]|.| =
sqrt ((1 ^2 ) + (0 ^2 ))
by Lm6, JGRAPH_3:10
.=
1
by SQUARE_1:59, SQUARE_1:60, SQUARE_1:83
;
:: thesis: ( |.|[0,(- 1)]|.| = 1 & |.|[0,1]|.| = 1 )thus |.|[0,(- 1)]|.| =
sqrt ((0 ^2 ) + ((- 1) ^2 ))
by Lm6, JGRAPH_3:10
.=
1
by SQUARE_1:59, SQUARE_1:60, SQUARE_1:61, SQUARE_1:83
;
:: thesis: |.|[0,1]|.| = 1thus |.|[0,1]|.| =
sqrt ((0 ^2 ) + (1 ^2 ))
by Lm6, JGRAPH_3:10
.=
1
by SQUARE_1:59, SQUARE_1:60, SQUARE_1:83
;
:: thesis: verum
end;
Lm8:
0 in [.0,1.]
by RCOMP_1:48;
Lm9:
1 in [.0,1.]
by RCOMP_1:48;
theorem Th23: :: JGRAPH_6:23
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th24: :: JGRAPH_6:24
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th25: :: JGRAPH_6:25
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
P being non
empty compact Subset of
(TOP-REAL 2) for
C0 being
Subset of
(TOP-REAL 2) st
P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } &
LE p1,
p2,
P &
LE p2,
p3,
P &
LE p3,
p4,
P holds
for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
C0 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } &
f . 0
= p3 &
f . 1
= p1 &
g . 0
= p2 &
g . 1
= p4 &
rng f c= C0 &
rng g c= C0 holds
rng f meets rng g
theorem Th26: :: JGRAPH_6:26
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
P being non
empty compact Subset of
(TOP-REAL 2) for
C0 being
Subset of
(TOP-REAL 2) st
P = { p where p is Point of (TOP-REAL 2) : |.p.| = 1 } &
LE p1,
p2,
P &
LE p2,
p3,
P &
LE p3,
p4,
P holds
for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
C0 = { p8 where p8 is Point of (TOP-REAL 2) : |.p8.| <= 1 } &
f . 0
= p3 &
f . 1
= p1 &
g . 0
= p4 &
g . 1
= p2 &
rng f c= C0 &
rng g c= C0 holds
rng f meets rng g
theorem Th27: :: JGRAPH_6:27
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
Lm10:
for a, b, c, d being real number st a <= b & c <= d holds
rectangle a,b,c,d = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = a & c <= p `2 & p `2 <= d ) or ( p `2 = d & a <= p `1 & p `1 <= b ) or ( p `1 = b & c <= p `2 & p `2 <= d ) or ( p `2 = c & a <= p `1 & p `1 <= b ) ) }
theorem Th28: :: JGRAPH_6:28
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem defines inside_of_rectangle JGRAPH_6:def 1 :
:: deftheorem defines closed_inside_of_rectangle JGRAPH_6:def 2 :
:: deftheorem defines outside_of_rectangle JGRAPH_6:def 3 :
:: deftheorem defines closed_outside_of_rectangle JGRAPH_6:def 4 :
theorem Th29: :: JGRAPH_6:29
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th30: :: JGRAPH_6:30
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th31: :: JGRAPH_6:31
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th32: :: JGRAPH_6:32
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem defines circle JGRAPH_6:def 5 :
:: deftheorem defines inside_of_circle JGRAPH_6:def 6 :
:: deftheorem defines closed_inside_of_circle JGRAPH_6:def 7 :
:: deftheorem defines outside_of_circle JGRAPH_6:def 8 :
:: deftheorem defines closed_outside_of_circle JGRAPH_6:def 9 :
theorem Th33: :: JGRAPH_6:33
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
r being
real number holds
(
inside_of_circle 0,0,
r = { p where p is Point of (TOP-REAL 2) : |.p.| < r } & (
r > 0 implies
circle 0,0,
r = { p2 where p2 is Point of (TOP-REAL 2) : |.p2.| = r } ) &
outside_of_circle 0,0,
r = { p3 where p3 is Point of (TOP-REAL 2) : |.p3.| > r } &
closed_inside_of_circle 0,0,
r = { q where q is Point of (TOP-REAL 2) : |.q.| <= r } &
closed_outside_of_circle 0,0,
r = { q2 where q2 is Point of (TOP-REAL 2) : |.q2.| >= r } )
theorem Th34: :: JGRAPH_6:34
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th35: :: JGRAPH_6:35
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th36: :: JGRAPH_6:36
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th37: :: JGRAPH_6:37
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: JGRAPH_6:38
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
P0,
P1,
P01,
P11,
K0,
K1,
K01,
K11 being
Subset of
(TOP-REAL 2) for
P being non
empty compact Subset of
(TOP-REAL 2) for
f being
Function of
(TOP-REAL 2),
(TOP-REAL 2) st
P = circle 0,0,1 &
P0 = inside_of_circle 0,0,1 &
P1 = outside_of_circle 0,0,1 &
P01 = closed_inside_of_circle 0,0,1 &
P11 = closed_outside_of_circle 0,0,1 &
K0 = inside_of_rectangle (- 1),1,
(- 1),1 &
K1 = outside_of_rectangle (- 1),1,
(- 1),1 &
K01 = closed_inside_of_rectangle (- 1),1,
(- 1),1 &
K11 = closed_outside_of_rectangle (- 1),1,
(- 1),1 &
f = Sq_Circ holds
(
f .: (rectangle (- 1),1,(- 1),1) = P &
(f " ) .: P = rectangle (- 1),1,
(- 1),1 &
f .: K0 = P0 &
(f " ) .: P0 = K0 &
f .: K1 = P1 &
(f " ) .: P1 = K1 &
f .: K01 = P01 &
f .: K11 = P11 &
(f " ) .: P01 = K01 &
(f " ) .: P11 = K11 )
theorem Th39: :: JGRAPH_6:39
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
a,
b,
c,
d being
real number st
a <= b &
c <= d holds
(
LSeg |[a,c]|,
|[a,d]| = { p1 where p1 is Point of (TOP-REAL 2) : ( p1 `1 = a & p1 `2 <= d & p1 `2 >= c ) } &
LSeg |[a,d]|,
|[b,d]| = { p2 where p2 is Point of (TOP-REAL 2) : ( p2 `1 <= b & p2 `1 >= a & p2 `2 = d ) } &
LSeg |[a,c]|,
|[b,c]| = { q1 where q1 is Point of (TOP-REAL 2) : ( q1 `1 <= b & q1 `1 >= a & q1 `2 = c ) } &
LSeg |[b,c]|,
|[b,d]| = { q2 where q2 is Point of (TOP-REAL 2) : ( q2 `1 = b & q2 `2 <= d & q2 `2 >= c ) } )
theorem :: JGRAPH_6:40
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem Th41: :: JGRAPH_6:41
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
a,
b,
c,
d being
real number st
a <= b &
c <= d holds
(LSeg |[a,c]|,|[a,d]|) /\ (LSeg |[a,c]|,|[b,c]|) = {|[a,c]|}
theorem Th42: :: JGRAPH_6:42
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
a,
b,
c,
d being
real number st
a <= b &
c <= d holds
(LSeg |[a,c]|,|[b,c]|) /\ (LSeg |[b,c]|,|[b,d]|) = {|[b,c]|}
theorem Th43: :: JGRAPH_6:43
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
a,
b,
c,
d being
real number st
a <= b &
c <= d holds
(LSeg |[a,d]|,|[b,d]|) /\ (LSeg |[b,c]|,|[b,d]|) = {|[b,d]|}
theorem Th44: :: JGRAPH_6:44
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
a,
b,
c,
d being
real number st
a <= b &
c <= d holds
(LSeg |[a,c]|,|[a,d]|) /\ (LSeg |[a,d]|,|[b,d]|) = {|[a,d]|}
theorem Th45: :: JGRAPH_6:45
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th46: :: JGRAPH_6:46
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th47: :: JGRAPH_6:47
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th48: :: JGRAPH_6:48
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th49: :: JGRAPH_6:49
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th50: :: JGRAPH_6:50
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th51: :: JGRAPH_6:51
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: JGRAPH_6:52
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: JGRAPH_6:53
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th54: :: JGRAPH_6:54
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th55: :: JGRAPH_6:55
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th56: :: JGRAPH_6:56
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
a,
b,
c,
d being
real number st
a <= b &
c <= d holds
(
W-min (rectangle a,b,c,d) = |[a,c]| &
E-max (rectangle a,b,c,d) = |[b,d]| )
theorem Th57: :: JGRAPH_6:57
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
a,
b,
c,
d being
real number st
a < b &
c < d holds
(
(LSeg |[a,c]|,|[a,d]|) \/ (LSeg |[a,d]|,|[b,d]|) is_an_arc_of W-min (rectangle a,b,c,d),
E-max (rectangle a,b,c,d) &
(LSeg |[a,c]|,|[b,c]|) \/ (LSeg |[b,c]|,|[b,d]|) is_an_arc_of E-max (rectangle a,b,c,d),
W-min (rectangle a,b,c,d) )
theorem Th58: :: JGRAPH_6:58
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
a,
b,
c,
d being
real number for
f1,
f2 being
FinSequence of
(TOP-REAL 2) for
p0,
p1,
p01,
p10 being
Point of
(TOP-REAL 2) st
a < b &
c < d &
p0 = |[a,c]| &
p1 = |[b,d]| &
p01 = |[a,d]| &
p10 = |[b,c]| &
f1 = <*p0,p01,p1*> &
f2 = <*p0,p10,p1*> holds
(
f1 is_S-Seq &
L~ f1 = (LSeg p0,p01) \/ (LSeg p01,p1) &
f2 is_S-Seq &
L~ f2 = (LSeg p0,p10) \/ (LSeg p10,p1) &
rectangle a,
b,
c,
d = (L~ f1) \/ (L~ f2) &
(L~ f1) /\ (L~ f2) = {p0,p1} &
f1 /. 1
= p0 &
f1 /. (len f1) = p1 &
f2 /. 1
= p0 &
f2 /. (len f2) = p1 )
theorem Th59: :: JGRAPH_6:59
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
P1,
P2 being
Subset of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f1,
f2 being
FinSequence of
(TOP-REAL 2) for
p1,
p2 being
Point of
(TOP-REAL 2) st
a < b &
c < d &
p1 = |[a,c]| &
p2 = |[b,d]| &
f1 = <*|[a,c]|,|[a,d]|,|[b,d]|*> &
f2 = <*|[a,c]|,|[b,c]|,|[b,d]|*> &
P1 = L~ f1 &
P2 = L~ f2 holds
(
P1 is_an_arc_of p1,
p2 &
P2 is_an_arc_of p1,
p2 & not
P1 is
empty & not
P2 is
empty &
rectangle a,
b,
c,
d = P1 \/ P2 &
P1 /\ P2 = {p1,p2} )
theorem Th60: :: JGRAPH_6:60
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th61: :: JGRAPH_6:61
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
a,
b,
c,
d being
real number st
a < b &
c < d holds
Upper_Arc (rectangle a,b,c,d) = (LSeg |[a,c]|,|[a,d]|) \/ (LSeg |[a,d]|,|[b,d]|)
theorem Th62: :: JGRAPH_6:62
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
a,
b,
c,
d being
real number st
a < b &
c < d holds
Lower_Arc (rectangle a,b,c,d) = (LSeg |[a,c]|,|[b,c]|) \/ (LSeg |[b,c]|,|[b,d]|)
theorem Th63: :: JGRAPH_6:63
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
a,
b,
c,
d being
real number st
a < b &
c < d holds
ex
f being
Function of
I[01] ,
((TOP-REAL 2) | (Upper_Arc (rectangle a,b,c,d))) st
(
f is_homeomorphism &
f . 0
= W-min (rectangle a,b,c,d) &
f . 1
= E-max (rectangle a,b,c,d) &
rng f = Upper_Arc (rectangle a,b,c,d) & ( for
r being
Real st
r in [.0,(1 / 2).] holds
f . r = ((1 - (2 * r)) * |[a,c]|) + ((2 * r) * |[a,d]|) ) & ( for
r being
Real st
r in [.(1 / 2),1.] holds
f . r = ((1 - ((2 * r) - 1)) * |[a,d]|) + (((2 * r) - 1) * |[b,d]|) ) & ( for
p being
Point of
(TOP-REAL 2) st
p in LSeg |[a,c]|,
|[a,d]| holds
( 0
<= (((p `2 ) - c) / (d - c)) / 2 &
(((p `2 ) - c) / (d - c)) / 2
<= 1 &
f . ((((p `2 ) - c) / (d - c)) / 2) = p ) ) & ( for
p being
Point of
(TOP-REAL 2) st
p in LSeg |[a,d]|,
|[b,d]| holds
( 0
<= ((((p `1 ) - a) / (b - a)) / 2) + (1 / 2) &
((((p `1 ) - a) / (b - a)) / 2) + (1 / 2) <= 1 &
f . (((((p `1 ) - a) / (b - a)) / 2) + (1 / 2)) = p ) ) )
theorem Th64: :: JGRAPH_6:64
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
a,
b,
c,
d being
real number st
a < b &
c < d holds
ex
f being
Function of
I[01] ,
((TOP-REAL 2) | (Lower_Arc (rectangle a,b,c,d))) st
(
f is_homeomorphism &
f . 0
= E-max (rectangle a,b,c,d) &
f . 1
= W-min (rectangle a,b,c,d) &
rng f = Lower_Arc (rectangle a,b,c,d) & ( for
r being
Real st
r in [.0,(1 / 2).] holds
f . r = ((1 - (2 * r)) * |[b,d]|) + ((2 * r) * |[b,c]|) ) & ( for
r being
Real st
r in [.(1 / 2),1.] holds
f . r = ((1 - ((2 * r) - 1)) * |[b,c]|) + (((2 * r) - 1) * |[a,c]|) ) & ( for
p being
Point of
(TOP-REAL 2) st
p in LSeg |[b,d]|,
|[b,c]| holds
( 0
<= (((p `2 ) - d) / (c - d)) / 2 &
(((p `2 ) - d) / (c - d)) / 2
<= 1 &
f . ((((p `2 ) - d) / (c - d)) / 2) = p ) ) & ( for
p being
Point of
(TOP-REAL 2) st
p in LSeg |[b,c]|,
|[a,c]| holds
( 0
<= ((((p `1 ) - b) / (a - b)) / 2) + (1 / 2) &
((((p `1 ) - b) / (a - b)) / 2) + (1 / 2) <= 1 &
f . (((((p `1 ) - b) / (a - b)) / 2) + (1 / 2)) = p ) ) )
theorem Th65: :: JGRAPH_6:65
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
a,
b,
c,
d being
real number for
p1,
p2 being
Point of
(TOP-REAL 2) st
a < b &
c < d &
p1 in LSeg |[a,c]|,
|[a,d]| &
p2 in LSeg |[a,c]|,
|[a,d]| holds
(
LE p1,
p2,
rectangle a,
b,
c,
d iff
p1 `2 <= p2 `2 )
theorem Th66: :: JGRAPH_6:66
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
a,
b,
c,
d being
real number for
p1,
p2 being
Point of
(TOP-REAL 2) st
a < b &
c < d &
p1 in LSeg |[a,d]|,
|[b,d]| &
p2 in LSeg |[a,d]|,
|[b,d]| holds
(
LE p1,
p2,
rectangle a,
b,
c,
d iff
p1 `1 <= p2 `1 )
theorem Th67: :: JGRAPH_6:67
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
a,
b,
c,
d being
real number for
p1,
p2 being
Point of
(TOP-REAL 2) st
a < b &
c < d &
p1 in LSeg |[b,c]|,
|[b,d]| &
p2 in LSeg |[b,c]|,
|[b,d]| holds
(
LE p1,
p2,
rectangle a,
b,
c,
d iff
p1 `2 >= p2 `2 )
theorem Th68: :: JGRAPH_6:68
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
a,
b,
c,
d being
real number for
p1,
p2 being
Point of
(TOP-REAL 2) st
a < b &
c < d &
p1 in LSeg |[a,c]|,
|[b,c]| &
p2 in LSeg |[a,c]|,
|[b,c]| holds
(
LE p1,
p2,
rectangle a,
b,
c,
d &
p1 <> W-min (rectangle a,b,c,d) iff (
p1 `1 >= p2 `1 &
p2 <> W-min (rectangle a,b,c,d) ) )
theorem Th69: :: JGRAPH_6:69
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
a,
b,
c,
d being
real number for
p1,
p2 being
Point of
(TOP-REAL 2) st
a < b &
c < d &
p1 in LSeg |[a,c]|,
|[a,d]| holds
(
LE p1,
p2,
rectangle a,
b,
c,
d iff ( (
p2 in LSeg |[a,c]|,
|[a,d]| &
p1 `2 <= p2 `2 ) or
p2 in LSeg |[a,d]|,
|[b,d]| or
p2 in LSeg |[b,d]|,
|[b,c]| or (
p2 in LSeg |[b,c]|,
|[a,c]| &
p2 <> W-min (rectangle a,b,c,d) ) ) )
theorem Th70: :: JGRAPH_6:70
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
a,
b,
c,
d being
real number for
p1,
p2 being
Point of
(TOP-REAL 2) st
a < b &
c < d &
p1 in LSeg |[a,d]|,
|[b,d]| holds
(
LE p1,
p2,
rectangle a,
b,
c,
d iff ( (
p2 in LSeg |[a,d]|,
|[b,d]| &
p1 `1 <= p2 `1 ) or
p2 in LSeg |[b,d]|,
|[b,c]| or (
p2 in LSeg |[b,c]|,
|[a,c]| &
p2 <> W-min (rectangle a,b,c,d) ) ) )
theorem Th71: :: JGRAPH_6:71
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
a,
b,
c,
d being
real number for
p1,
p2 being
Point of
(TOP-REAL 2) st
a < b &
c < d &
p1 in LSeg |[b,d]|,
|[b,c]| holds
(
LE p1,
p2,
rectangle a,
b,
c,
d iff ( (
p2 in LSeg |[b,d]|,
|[b,c]| &
p1 `2 >= p2 `2 ) or (
p2 in LSeg |[b,c]|,
|[a,c]| &
p2 <> W-min (rectangle a,b,c,d) ) ) )
theorem Th72: :: JGRAPH_6:72
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
a,
b,
c,
d being
real number for
p1,
p2 being
Point of
(TOP-REAL 2) st
a < b &
c < d &
p1 in LSeg |[b,c]|,
|[a,c]| &
p1 <> W-min (rectangle a,b,c,d) holds
(
LE p1,
p2,
rectangle a,
b,
c,
d iff (
p2 in LSeg |[b,c]|,
|[a,c]| &
p1 `1 >= p2 `1 &
p2 <> W-min (rectangle a,b,c,d) ) )
theorem Th73: :: JGRAPH_6:73
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
x being
set for
a,
b,
c,
d being
real number st
x in rectangle a,
b,
c,
d &
a < b &
c < d & not
x in LSeg |[a,c]|,
|[a,d]| & not
x in LSeg |[a,d]|,
|[b,d]| & not
x in LSeg |[b,d]|,
|[b,c]| holds
x in LSeg |[b,c]|,
|[a,c]|
theorem Th74: :: JGRAPH_6:74
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
p1,
p2 being
Point of
(TOP-REAL 2) st
LE p1,
p2,
rectangle (- 1),1,
(- 1),1 &
p1 in LSeg |[(- 1),(- 1)]|,
|[(- 1),1]| & not (
p2 in LSeg |[(- 1),(- 1)]|,
|[(- 1),1]| &
p2 `2 >= p1 `2 ) & not
p2 in LSeg |[(- 1),1]|,
|[1,1]| & not
p2 in LSeg |[1,1]|,
|[1,(- 1)]| holds
(
p2 in LSeg |[1,(- 1)]|,
|[(- 1),(- 1)]| &
p2 <> |[(- 1),(- 1)]| )
theorem Th75: :: JGRAPH_6:75
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
p1,
p2 being
Point of
(TOP-REAL 2) for
P being non
empty compact Subset of
(TOP-REAL 2) for
f being
Function of
(TOP-REAL 2),
(TOP-REAL 2) st
P = circle 0,0,1 &
f = Sq_Circ &
p1 in LSeg |[(- 1),(- 1)]|,
|[(- 1),1]| &
p1 `2 >= 0 &
LE p1,
p2,
rectangle (- 1),1,
(- 1),1 holds
LE f . p1,
f . p2,
P
theorem Th76: :: JGRAPH_6:76
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
p1,
p2,
p3 being
Point of
(TOP-REAL 2) for
P being non
empty compact Subset of
(TOP-REAL 2) for
f being
Function of
(TOP-REAL 2),
(TOP-REAL 2) st
P = circle 0,0,1 &
f = Sq_Circ &
p1 in LSeg |[(- 1),(- 1)]|,
|[(- 1),1]| &
p1 `2 >= 0 &
LE p1,
p2,
rectangle (- 1),1,
(- 1),1 &
LE p2,
p3,
rectangle (- 1),1,
(- 1),1 holds
LE f . p2,
f . p3,
P
theorem Th77: :: JGRAPH_6:77
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th78: :: JGRAPH_6:78
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th79: :: JGRAPH_6:79
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th80: :: JGRAPH_6:80
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th81: :: JGRAPH_6:81
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th82: :: JGRAPH_6:82
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
P being non
empty compact Subset of
(TOP-REAL 2) for
f being
Function of
(TOP-REAL 2),
(TOP-REAL 2) st
P = circle 0,0,1 &
f = Sq_Circ &
LE p1,
p2,
rectangle (- 1),1,
(- 1),1 &
LE p2,
p3,
rectangle (- 1),1,
(- 1),1 &
LE p3,
p4,
rectangle (- 1),1,
(- 1),1 holds
f . p1,
f . p2,
f . p3,
f . p4 are_in_this_order_on P
theorem Th83: :: JGRAPH_6:83
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: JGRAPH_6:84
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
p1,
p2,
p3 being
Point of
(TOP-REAL 2) for
P being non
empty compact Subset of
(TOP-REAL 2) st
P is_simple_closed_curve &
p1 in P &
p2 in P &
p3 in P & not (
LE p1,
p2,
P &
LE p2,
p3,
P ) & not (
LE p1,
p3,
P &
LE p3,
p2,
P ) & not (
LE p2,
p1,
P &
LE p1,
p3,
P ) & not (
LE p2,
p3,
P &
LE p3,
p1,
P ) & not (
LE p3,
p1,
P &
LE p1,
p2,
P ) holds
(
LE p3,
p2,
P &
LE p2,
p1,
P )
by Th83;
theorem :: JGRAPH_6:85
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
p1,
p2,
p3 being
Point of
(TOP-REAL 2) for
P being non
empty compact Subset of
(TOP-REAL 2) st
P is_simple_closed_curve &
p1 in P &
p2 in P &
p3 in P &
LE p2,
p3,
P & not
LE p1,
p2,
P & not (
LE p2,
p1,
P &
LE p1,
p3,
P ) holds
LE p3,
p1,
P by Th83;
theorem :: JGRAPH_6:86
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
P being non
empty compact Subset of
(TOP-REAL 2) st
P is_simple_closed_curve &
p1 in P &
p2 in P &
p3 in P &
p4 in P &
LE p2,
p3,
P &
LE p3,
p4,
P & not
LE p1,
p2,
P & not (
LE p2,
p1,
P &
LE p1,
p3,
P ) & not (
LE p3,
p1,
P &
LE p1,
p4,
P ) holds
LE p4,
p1,
P by Th83;
theorem Th87: :: JGRAPH_6:87
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
P being non
empty compact Subset of
(TOP-REAL 2) for
f being
Function of
(TOP-REAL 2),
(TOP-REAL 2) st
P = circle 0,0,1 &
f = Sq_Circ &
LE f . p1,
f . p2,
P &
LE f . p2,
f . p3,
P &
LE f . p3,
f . p4,
P holds
p1,
p2,
p3,
p4 are_in_this_order_on rectangle (- 1),1,
(- 1),1
theorem Th88: :: JGRAPH_6:88
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
P being non
empty compact Subset of
(TOP-REAL 2) for
f being
Function of
(TOP-REAL 2),
(TOP-REAL 2) st
P = circle 0,0,1 &
f = Sq_Circ holds
(
p1,
p2,
p3,
p4 are_in_this_order_on rectangle (- 1),1,
(- 1),1 iff
f . p1,
f . p2,
f . p3,
f . p4 are_in_this_order_on P )
theorem :: JGRAPH_6:89
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
K0 being
Subset of
(TOP-REAL 2) st
p1,
p2,
p3,
p4 are_in_this_order_on rectangle (- 1),1,
(- 1),1 holds
for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
K0 = closed_inside_of_rectangle (- 1),1,
(- 1),1 &
f . 0
= p1 &
f . 1
= p3 &
g . 0
= p2 &
g . 1
= p4 &
rng f c= K0 &
rng g c= K0 holds
rng f meets rng g