:: Fashoda Meet Theorem for Rectangles
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received January 3, 2005
:: Copyright (c) 2005 Association of Mizar Users
theorem Th1: :: JGRAPH_7:1
theorem Th2: :: JGRAPH_7:2
theorem Th3: :: JGRAPH_7:3
theorem Th4: :: JGRAPH_7:4
theorem Th5: :: JGRAPH_7:5
theorem Th6: :: JGRAPH_7:6
theorem Th7: :: JGRAPH_7:7
theorem Th8: :: JGRAPH_7:8
theorem Th9: :: JGRAPH_7:9
theorem Th10: :: JGRAPH_7:10
theorem Th11: :: JGRAPH_7:11
theorem Th12: :: JGRAPH_7:12
theorem Th13: :: JGRAPH_7:13
theorem Th14: :: JGRAPH_7:14
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number st
a < b &
c < d &
p1 `1 = a &
p2 `1 = a &
p3 `1 = a &
p4 `1 = a &
c <= p1 `2 &
p1 `2 < p2 `2 &
p2 `2 < p3 `2 &
p3 `2 < p4 `2 &
p4 `2 <= d holds
p1,
p2,
p3,
p4 are_in_this_order_on rectangle a,
b,
c,
d
theorem Th15: :: JGRAPH_7:15
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number st
a < b &
c < d &
p1 `1 = a &
p2 `1 = a &
p3 `1 = a &
p4 `2 = d &
c <= p1 `2 &
p1 `2 < p2 `2 &
p2 `2 < p3 `2 &
p3 `2 <= d &
a <= p4 `1 &
p4 `1 <= b holds
p1,
p2,
p3,
p4 are_in_this_order_on rectangle a,
b,
c,
d
theorem Th16: :: JGRAPH_7:16
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number st
a < b &
c < d &
p1 `1 = a &
p2 `1 = a &
p3 `1 = a &
p4 `1 = b &
c <= p1 `2 &
p1 `2 < p2 `2 &
p2 `2 < p3 `2 &
p3 `2 <= d &
c <= p4 `2 &
p4 `2 <= d holds
p1,
p2,
p3,
p4 are_in_this_order_on rectangle a,
b,
c,
d
theorem Th17: :: JGRAPH_7:17
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number st
a < b &
c < d &
p1 `1 = a &
p2 `1 = a &
p3 `1 = a &
p4 `2 = c &
c <= p1 `2 &
p1 `2 < p2 `2 &
p2 `2 < p3 `2 &
p3 `2 <= d &
a < p4 `1 &
p4 `1 <= b holds
p1,
p2,
p3,
p4 are_in_this_order_on rectangle a,
b,
c,
d
theorem Th18: :: JGRAPH_7:18
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number st
a < b &
c < d &
p1 `1 = a &
p2 `1 = a &
p3 `2 = d &
p4 `2 = d &
c <= p1 `2 &
p1 `2 < p2 `2 &
p2 `2 <= d &
a <= p3 `1 &
p3 `1 < p4 `1 &
p4 `1 <= b holds
p1,
p2,
p3,
p4 are_in_this_order_on rectangle a,
b,
c,
d
theorem Th19: :: JGRAPH_7:19
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number st
a < b &
c < d &
p1 `1 = a &
p2 `1 = a &
p3 `2 = d &
p4 `1 = b &
c <= p1 `2 &
p1 `2 < p2 `2 &
p2 `2 <= d &
a <= p3 `1 &
p3 `1 <= b &
c <= p4 `2 &
p4 `2 <= d holds
p1,
p2,
p3,
p4 are_in_this_order_on rectangle a,
b,
c,
d
theorem Th20: :: JGRAPH_7:20
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number st
a < b &
c < d &
p1 `1 = a &
p2 `1 = a &
p3 `2 = d &
p4 `2 = c &
c <= p1 `2 &
p1 `2 < p2 `2 &
p2 `2 <= d &
a <= p3 `1 &
p3 `1 <= b &
a < p4 `1 &
p4 `1 <= b holds
p1,
p2,
p3,
p4 are_in_this_order_on rectangle a,
b,
c,
d
theorem Th21: :: JGRAPH_7:21
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number st
a < b &
c < d &
p1 `1 = a &
p2 `1 = a &
p3 `1 = b &
p4 `1 = b &
c <= p1 `2 &
p1 `2 < p2 `2 &
p2 `2 <= d &
c <= p4 `2 &
p4 `2 < p3 `2 &
p3 `2 <= d holds
p1,
p2,
p3,
p4 are_in_this_order_on rectangle a,
b,
c,
d
theorem Th22: :: JGRAPH_7:22
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number st
a < b &
c < d &
p1 `1 = a &
p2 `1 = a &
p3 `1 = b &
p4 `2 = c &
c <= p1 `2 &
p1 `2 < p2 `2 &
p2 `2 <= d &
c <= p3 `2 &
p3 `2 <= d &
a < p4 `1 &
p4 `1 <= b holds
p1,
p2,
p3,
p4 are_in_this_order_on rectangle a,
b,
c,
d
theorem Th23: :: JGRAPH_7:23
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number st
a < b &
c < d &
p1 `1 = a &
p2 `1 = a &
p3 `2 = c &
p4 `2 = c &
c <= p1 `2 &
p1 `2 < p2 `2 &
p2 `2 <= d &
a < p4 `1 &
p4 `1 < p3 `1 &
p3 `1 <= b holds
p1,
p2,
p3,
p4 are_in_this_order_on rectangle a,
b,
c,
d
theorem Th24: :: JGRAPH_7:24
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number st
a < b &
c < d &
p1 `1 = a &
p2 `2 = d &
p3 `2 = d &
p4 `2 = d &
c <= p1 `2 &
p1 `2 <= d &
a <= p2 `1 &
p2 `1 < p3 `1 &
p3 `1 < p4 `1 &
p4 `1 <= b holds
p1,
p2,
p3,
p4 are_in_this_order_on rectangle a,
b,
c,
d
theorem Th25: :: JGRAPH_7:25
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number st
a < b &
c < d &
p1 `1 = a &
p2 `2 = d &
p3 `2 = d &
p4 `1 = b &
c <= p1 `2 &
p1 `2 <= d &
a <= p2 `1 &
p2 `1 < p3 `1 &
p3 `1 <= b &
c <= p4 `2 &
p4 `2 <= d holds
p1,
p2,
p3,
p4 are_in_this_order_on rectangle a,
b,
c,
d
theorem Th26: :: JGRAPH_7:26
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number st
a < b &
c < d &
p1 `1 = a &
p2 `2 = d &
p3 `2 = d &
p4 `2 = c &
c <= p1 `2 &
p1 `2 <= d &
a <= p2 `1 &
p2 `1 < p3 `1 &
p3 `1 <= b &
a < p4 `1 &
p4 `1 <= b holds
p1,
p2,
p3,
p4 are_in_this_order_on rectangle a,
b,
c,
d
theorem Th27: :: JGRAPH_7:27
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number st
a < b &
c < d &
p1 `1 = a &
p2 `2 = d &
p3 `1 = b &
p4 `1 = b &
c <= p1 `2 &
p1 `2 <= d &
a <= p2 `1 &
p2 `1 <= b &
c <= p4 `2 &
p4 `2 < p3 `2 &
p3 `2 <= d holds
p1,
p2,
p3,
p4 are_in_this_order_on rectangle a,
b,
c,
d
theorem Th28: :: JGRAPH_7:28
theorem Th29: :: JGRAPH_7:29
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number st
a < b &
c < d &
p1 `1 = a &
p2 `2 = d &
p3 `2 = c &
p4 `2 = c &
c <= p1 `2 &
p1 `2 <= d &
a <= p2 `1 &
p2 `1 <= b &
a < p4 `1 &
p4 `1 < p3 `1 &
p3 `1 <= b holds
p1,
p2,
p3,
p4 are_in_this_order_on rectangle a,
b,
c,
d
theorem Th30: :: JGRAPH_7:30
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number st
a < b &
c < d &
p1 `1 = a &
p2 `1 = b &
p3 `1 = b &
p4 `1 = b &
c <= p1 `2 &
p1 `2 <= d &
d >= p2 `2 &
p2 `2 > p3 `2 &
p3 `2 > p4 `2 &
p4 `2 >= c holds
p1,
p2,
p3,
p4 are_in_this_order_on rectangle a,
b,
c,
d
theorem Th31: :: JGRAPH_7:31
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number st
a < b &
c < d &
p1 `1 = a &
p2 `1 = b &
p3 `1 = b &
p4 `2 = c &
c <= p1 `2 &
p1 `2 <= d &
d >= p2 `2 &
p2 `2 > p3 `2 &
p3 `2 >= c &
a < p4 `1 &
p4 `1 <= b holds
p1,
p2,
p3,
p4 are_in_this_order_on rectangle a,
b,
c,
d
theorem Th32: :: JGRAPH_7:32
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number st
a < b &
c < d &
p1 `1 = a &
p2 `1 = b &
p3 `2 = c &
p4 `2 = c &
c <= p1 `2 &
p1 `2 <= d &
c <= p2 `2 &
p2 `2 <= d &
a < p4 `1 &
p4 `1 < p3 `1 &
p3 `1 <= b holds
p1,
p2,
p3,
p4 are_in_this_order_on rectangle a,
b,
c,
d
theorem Th33: :: JGRAPH_7:33
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number st
a < b &
c < d &
p1 `1 = a &
p2 `2 = c &
p3 `2 = c &
p4 `2 = c &
c <= p1 `2 &
p1 `2 <= d &
a < p4 `1 &
p4 `1 < p3 `1 &
p3 `1 < p2 `1 &
p2 `1 <= b holds
p1,
p2,
p3,
p4 are_in_this_order_on rectangle a,
b,
c,
d
theorem Th34: :: JGRAPH_7:34
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number st
a < b &
c < d &
p1 `2 = d &
p2 `2 = d &
p3 `2 = d &
p4 `2 = d &
a <= p1 `1 &
p1 `1 < p2 `1 &
p2 `1 < p3 `1 &
p3 `1 < p4 `1 &
p4 `1 <= b holds
p1,
p2,
p3,
p4 are_in_this_order_on rectangle a,
b,
c,
d
theorem Th35: :: JGRAPH_7:35
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number st
a < b &
c < d &
p1 `2 = d &
p2 `2 = d &
p3 `2 = d &
p4 `1 = b &
a <= p1 `1 &
p1 `1 < p2 `1 &
p2 `1 < p3 `1 &
p3 `1 <= b &
c <= p4 `2 &
p4 `2 <= d holds
p1,
p2,
p3,
p4 are_in_this_order_on rectangle a,
b,
c,
d
theorem Th36: :: JGRAPH_7:36
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number st
a < b &
c < d &
p1 `2 = d &
p2 `2 = d &
p3 `2 = d &
p4 `2 = c &
a <= p1 `1 &
p1 `1 < p2 `1 &
p2 `1 < p3 `1 &
p3 `1 <= b &
a < p4 `1 &
p4 `1 <= b holds
p1,
p2,
p3,
p4 are_in_this_order_on rectangle a,
b,
c,
d
theorem Th37: :: JGRAPH_7:37
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number st
a < b &
c < d &
p1 `2 = d &
p2 `2 = d &
p3 `1 = b &
p4 `1 = b &
a <= p1 `1 &
p1 `1 < p2 `1 &
p2 `1 <= b &
c <= p4 `2 &
p4 `2 < p3 `2 &
p3 `2 <= d holds
p1,
p2,
p3,
p4 are_in_this_order_on rectangle a,
b,
c,
d
theorem Th38: :: JGRAPH_7:38
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number st
a < b &
c < d &
p1 `2 = d &
p2 `2 = d &
p3 `1 = b &
p4 `2 = c &
a <= p1 `1 &
p1 `1 < p2 `1 &
p2 `1 <= b &
c <= p3 `2 &
p3 `2 <= d &
a < p4 `1 &
p4 `1 <= b holds
p1,
p2,
p3,
p4 are_in_this_order_on rectangle a,
b,
c,
d
theorem Th39: :: JGRAPH_7:39
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number st
a < b &
c < d &
p1 `2 = d &
p2 `2 = d &
p3 `2 = c &
p4 `2 = c &
a <= p1 `1 &
p1 `1 < p2 `1 &
p2 `1 <= b &
a < p4 `1 &
p4 `1 < p3 `1 &
p3 `1 <= b holds
p1,
p2,
p3,
p4 are_in_this_order_on rectangle a,
b,
c,
d
theorem Th40: :: JGRAPH_7:40
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number st
a < b &
c < d &
p1 `2 = d &
p2 `1 = b &
p3 `1 = b &
p4 `1 = b &
a <= p1 `1 &
p1 `1 <= b &
d >= p2 `2 &
p2 `2 > p3 `2 &
p3 `2 > p4 `2 &
p4 `2 >= c holds
p1,
p2,
p3,
p4 are_in_this_order_on rectangle a,
b,
c,
d
theorem Th41: :: JGRAPH_7:41
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number st
a < b &
c < d &
p1 `2 = d &
p2 `1 = b &
p3 `1 = b &
p4 `2 = c &
a <= p1 `1 &
p1 `1 <= b &
d >= p2 `2 &
p2 `2 > p3 `2 &
p3 `2 >= c &
a < p4 `1 &
p4 `1 <= b holds
p1,
p2,
p3,
p4 are_in_this_order_on rectangle a,
b,
c,
d
theorem Th42: :: JGRAPH_7:42
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number st
a < b &
c < d &
p1 `2 = d &
p2 `1 = b &
p3 `2 = c &
p4 `2 = c &
a <= p1 `1 &
p1 `1 <= b &
c <= p2 `2 &
p2 `2 <= d &
a < p4 `1 &
p4 `1 < p3 `1 &
p3 `1 <= b holds
p1,
p2,
p3,
p4 are_in_this_order_on rectangle a,
b,
c,
d
theorem Th43: :: JGRAPH_7:43
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number st
a < b &
c < d &
p1 `2 = d &
p2 `2 = c &
p3 `2 = c &
p4 `2 = c &
a <= p1 `1 &
p1 `1 <= b &
a < p4 `1 &
p4 `1 < p3 `1 &
p3 `1 < p2 `1 &
p2 `1 <= b holds
p1,
p2,
p3,
p4 are_in_this_order_on rectangle a,
b,
c,
d
theorem Th44: :: JGRAPH_7:44
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number st
a < b &
c < d &
p1 `1 = b &
p2 `1 = b &
p3 `1 = b &
p4 `1 = b &
d >= p1 `2 &
p1 `2 > p2 `2 &
p2 `2 > p3 `2 &
p3 `2 > p4 `2 &
p4 `2 >= c holds
p1,
p2,
p3,
p4 are_in_this_order_on rectangle a,
b,
c,
d
theorem Th45: :: JGRAPH_7:45
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number st
a < b &
c < d &
p1 `1 = b &
p2 `1 = b &
p3 `1 = b &
p4 `2 = c &
d >= p1 `2 &
p1 `2 > p2 `2 &
p2 `2 > p3 `2 &
p3 `2 >= c &
a < p4 `1 &
p4 `1 <= b holds
p1,
p2,
p3,
p4 are_in_this_order_on rectangle a,
b,
c,
d
theorem Th46: :: JGRAPH_7:46
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number st
a < b &
c < d &
p1 `1 = b &
p2 `1 = b &
p3 `2 = c &
p4 `2 = c &
d >= p1 `2 &
p1 `2 > p2 `2 &
p2 `2 >= c &
b >= p3 `1 &
p3 `1 > p4 `1 &
p4 `1 > a holds
p1,
p2,
p3,
p4 are_in_this_order_on rectangle a,
b,
c,
d
theorem Th47: :: JGRAPH_7:47
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number st
a < b &
c < d &
p1 `1 = b &
p2 `2 = c &
p3 `2 = c &
p4 `2 = c &
c <= p1 `2 &
p1 `2 <= d &
b >= p2 `1 &
p2 `1 > p3 `1 &
p3 `1 > p4 `1 &
p4 `1 > a holds
p1,
p2,
p3,
p4 are_in_this_order_on rectangle a,
b,
c,
d
theorem Th48: :: JGRAPH_7:48
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number st
a < b &
c < d &
p1 `2 = c &
p2 `2 = c &
p3 `2 = c &
p4 `2 = c &
b >= p1 `1 &
p1 `1 > p2 `1 &
p2 `1 > p3 `1 &
p3 `1 > p4 `1 &
p4 `1 > a holds
p1,
p2,
p3,
p4 are_in_this_order_on rectangle a,
b,
c,
d
theorem Th49: :: JGRAPH_7:49
for
A,
B,
C,
D being
real number for
h,
g being
Function of
(TOP-REAL 2),
(TOP-REAL 2) st
A > 0 &
C > 0 &
h = AffineMap A,
B,
C,
D &
g = AffineMap (1 / A),
(- (B / A)),
(1 / C),
(- (D / C)) holds
(
g = h " &
h = g " )
theorem Th50: :: JGRAPH_7:50
theorem Th51: :: JGRAPH_7:51
theorem Th52: :: JGRAPH_7:52
for
a,
b,
c,
d being
real number for
h being
Function of
(TOP-REAL 2),
(TOP-REAL 2) for
f being
Function of
I[01] ,
(TOP-REAL 2) st
a < b &
c < d &
h = AffineMap (2 / (b - a)),
(- ((b + a) / (b - a))),
(2 / (d - c)),
(- ((d + c) / (d - c))) &
rng f c= closed_inside_of_rectangle a,
b,
c,
d holds
rng (h * f) c= closed_inside_of_rectangle (- 1),1,
(- 1),1
theorem Th53: :: JGRAPH_7:53
theorem Th54: :: JGRAPH_7:54
theorem Th55: :: JGRAPH_7:55
theorem Th56: :: JGRAPH_7:56
theorem Th57: :: JGRAPH_7:57
theorem Th58: :: JGRAPH_7:58
theorem Th59: :: JGRAPH_7:59
theorem Th60: :: JGRAPH_7:60
theorem Th61: :: JGRAPH_7:61
theorem Th62: :: JGRAPH_7:62
theorem Th63: :: JGRAPH_7:63
theorem Th64: :: JGRAPH_7:64
theorem Th65: :: JGRAPH_7:65
theorem Th66: :: JGRAPH_7:66
theorem Th67: :: JGRAPH_7:67
theorem Th68: :: JGRAPH_7:68
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `1 = a &
p3 `1 = a &
p4 `1 = a &
c <= p1 `2 &
p1 `2 < p2 `2 &
p2 `2 < p3 `2 &
p3 `2 < p4 `2 &
p4 `2 <= d &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
rng f c= closed_inside_of_rectangle a,
b,
c,
d &
rng g c= closed_inside_of_rectangle a,
b,
c,
d holds
rng f meets rng g
theorem :: JGRAPH_7:69
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
P,
Q being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `1 = a &
p3 `1 = a &
p4 `1 = a &
c <= p1 `2 &
p1 `2 < p2 `2 &
p2 `2 < p3 `2 &
p3 `2 < p4 `2 &
p4 `2 <= d &
P is_an_arc_of p1,
p3 &
Q is_an_arc_of p2,
p4 &
P c= closed_inside_of_rectangle a,
b,
c,
d &
Q c= closed_inside_of_rectangle a,
b,
c,
d holds
P meets Q
theorem Th70: :: JGRAPH_7:70
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `1 = a &
p3 `1 = a &
p4 `2 = d &
c <= p1 `2 &
p1 `2 < p2 `2 &
p2 `2 < p3 `2 &
p3 `2 <= d &
a <= p4 `1 &
p4 `1 <= b &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
rng f c= closed_inside_of_rectangle a,
b,
c,
d &
rng g c= closed_inside_of_rectangle a,
b,
c,
d holds
rng f meets rng g
theorem :: JGRAPH_7:71
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
P,
Q being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `1 = a &
p3 `1 = a &
p4 `2 = d &
c <= p1 `2 &
p1 `2 < p2 `2 &
p2 `2 < p3 `2 &
p3 `2 <= d &
a <= p4 `1 &
p4 `1 <= b &
P is_an_arc_of p1,
p3 &
Q is_an_arc_of p2,
p4 &
P c= closed_inside_of_rectangle a,
b,
c,
d &
Q c= closed_inside_of_rectangle a,
b,
c,
d holds
P meets Q
theorem Th72: :: JGRAPH_7:72
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `1 = a &
p3 `1 = a &
p4 `1 = b &
c <= p1 `2 &
p1 `2 < p2 `2 &
p2 `2 < p3 `2 &
p3 `2 <= d &
c <= p4 `2 &
p4 `2 <= d &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
rng f c= closed_inside_of_rectangle a,
b,
c,
d &
rng g c= closed_inside_of_rectangle a,
b,
c,
d holds
rng f meets rng g
theorem :: JGRAPH_7:73
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
P,
Q being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `1 = a &
p3 `1 = a &
p4 `1 = b &
c <= p1 `2 &
p1 `2 < p2 `2 &
p2 `2 < p3 `2 &
p3 `2 <= d &
c <= p4 `2 &
p4 `2 <= d &
P is_an_arc_of p1,
p3 &
Q is_an_arc_of p2,
p4 &
P c= closed_inside_of_rectangle a,
b,
c,
d &
Q c= closed_inside_of_rectangle a,
b,
c,
d holds
P meets Q
theorem Th74: :: JGRAPH_7:74
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `1 = a &
p3 `1 = a &
p4 `2 = c &
c <= p1 `2 &
p1 `2 < p2 `2 &
p2 `2 < p3 `2 &
p3 `2 <= d &
a < p4 `1 &
p4 `1 <= b &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
rng f c= closed_inside_of_rectangle a,
b,
c,
d &
rng g c= closed_inside_of_rectangle a,
b,
c,
d holds
rng f meets rng g
theorem :: JGRAPH_7:75
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
P,
Q being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `1 = a &
p3 `1 = a &
p4 `2 = c &
c <= p1 `2 &
p1 `2 < p2 `2 &
p2 `2 < p3 `2 &
p3 `2 <= d &
a < p4 `1 &
p4 `1 <= b &
P is_an_arc_of p1,
p3 &
Q is_an_arc_of p2,
p4 &
P c= closed_inside_of_rectangle a,
b,
c,
d &
Q c= closed_inside_of_rectangle a,
b,
c,
d holds
P meets Q
theorem Th76: :: JGRAPH_7:76
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `1 = a &
p3 `2 = d &
p4 `2 = d &
c <= p1 `2 &
p1 `2 < p2 `2 &
p2 `2 <= d &
a <= p3 `1 &
p3 `1 < p4 `1 &
p4 `1 <= b &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
rng f c= closed_inside_of_rectangle a,
b,
c,
d &
rng g c= closed_inside_of_rectangle a,
b,
c,
d holds
rng f meets rng g
theorem :: JGRAPH_7:77
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
P,
Q being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `1 = a &
p3 `2 = d &
p4 `2 = d &
c <= p1 `2 &
p1 `2 < p2 `2 &
p2 `2 <= d &
a <= p3 `1 &
p3 `1 < p4 `1 &
p4 `1 <= b &
P is_an_arc_of p1,
p3 &
Q is_an_arc_of p2,
p4 &
P c= closed_inside_of_rectangle a,
b,
c,
d &
Q c= closed_inside_of_rectangle a,
b,
c,
d holds
P meets Q
theorem Th78: :: JGRAPH_7:78
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `1 = a &
p3 `2 = d &
p4 `1 = b &
c <= p1 `2 &
p1 `2 < p2 `2 &
p2 `2 <= d &
a <= p3 `1 &
p3 `1 <= b &
c <= p4 `2 &
p4 `2 <= d &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
rng f c= closed_inside_of_rectangle a,
b,
c,
d &
rng g c= closed_inside_of_rectangle a,
b,
c,
d holds
rng f meets rng g
theorem :: JGRAPH_7:79
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
P,
Q being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `1 = a &
p3 `2 = d &
p4 `1 = b &
c <= p1 `2 &
p1 `2 < p2 `2 &
p2 `2 <= d &
a <= p3 `1 &
p3 `1 <= b &
c <= p4 `2 &
p4 `2 <= d &
P is_an_arc_of p1,
p3 &
Q is_an_arc_of p2,
p4 &
P c= closed_inside_of_rectangle a,
b,
c,
d &
Q c= closed_inside_of_rectangle a,
b,
c,
d holds
P meets Q
theorem Th80: :: JGRAPH_7:80
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `1 = a &
p3 `2 = d &
p4 `2 = c &
c <= p1 `2 &
p1 `2 < p2 `2 &
p2 `2 <= d &
a <= p3 `1 &
p3 `1 <= b &
a < p4 `1 &
p4 `1 <= b &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
rng f c= closed_inside_of_rectangle a,
b,
c,
d &
rng g c= closed_inside_of_rectangle a,
b,
c,
d holds
rng f meets rng g
theorem :: JGRAPH_7:81
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
P,
Q being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `1 = a &
p3 `2 = d &
p4 `2 = c &
c <= p1 `2 &
p1 `2 < p2 `2 &
p2 `2 <= d &
a <= p3 `1 &
p3 `1 <= b &
a < p4 `1 &
p4 `1 <= b &
P is_an_arc_of p1,
p3 &
Q is_an_arc_of p2,
p4 &
P c= closed_inside_of_rectangle a,
b,
c,
d &
Q c= closed_inside_of_rectangle a,
b,
c,
d holds
P meets Q
theorem Th82: :: JGRAPH_7:82
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `1 = a &
p3 `1 = b &
p4 `1 = b &
c <= p1 `2 &
p1 `2 < p2 `2 &
p2 `2 <= d &
c <= p4 `2 &
p4 `2 < p3 `2 &
p3 `2 <= d &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
rng f c= closed_inside_of_rectangle a,
b,
c,
d &
rng g c= closed_inside_of_rectangle a,
b,
c,
d holds
rng f meets rng g
theorem :: JGRAPH_7:83
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
P,
Q being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `1 = a &
p3 `1 = b &
p4 `1 = b &
c <= p1 `2 &
p1 `2 < p2 `2 &
p2 `2 <= d &
c <= p4 `2 &
p4 `2 < p3 `2 &
p3 `2 <= d &
P is_an_arc_of p1,
p3 &
Q is_an_arc_of p2,
p4 &
P c= closed_inside_of_rectangle a,
b,
c,
d &
Q c= closed_inside_of_rectangle a,
b,
c,
d holds
P meets Q
theorem Th84: :: JGRAPH_7:84
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `1 = a &
p3 `1 = b &
p4 `2 = c &
c <= p1 `2 &
p1 `2 < p2 `2 &
p2 `2 <= d &
c <= p3 `2 &
p3 `2 <= d &
a < p4 `1 &
p4 `1 <= b &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
rng f c= closed_inside_of_rectangle a,
b,
c,
d &
rng g c= closed_inside_of_rectangle a,
b,
c,
d holds
rng f meets rng g
theorem :: JGRAPH_7:85
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
P,
Q being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `1 = a &
p3 `1 = b &
p4 `2 = c &
c <= p1 `2 &
p1 `2 < p2 `2 &
p2 `2 <= d &
c <= p3 `2 &
p3 `2 <= d &
a < p4 `1 &
p4 `1 <= b &
P is_an_arc_of p1,
p3 &
Q is_an_arc_of p2,
p4 &
P c= closed_inside_of_rectangle a,
b,
c,
d &
Q c= closed_inside_of_rectangle a,
b,
c,
d holds
P meets Q
theorem Th86: :: JGRAPH_7:86
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `1 = a &
p3 `2 = c &
p4 `2 = c &
c <= p1 `2 &
p1 `2 < p2 `2 &
p2 `2 <= d &
a < p4 `1 &
p4 `1 < p3 `1 &
p3 `1 <= b &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
rng f c= closed_inside_of_rectangle a,
b,
c,
d &
rng g c= closed_inside_of_rectangle a,
b,
c,
d holds
rng f meets rng g
theorem :: JGRAPH_7:87
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
P,
Q being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `1 = a &
p3 `2 = c &
p4 `2 = c &
c <= p1 `2 &
p1 `2 < p2 `2 &
p2 `2 <= d &
a < p4 `1 &
p4 `1 < p3 `1 &
p3 `1 <= b &
P is_an_arc_of p1,
p3 &
Q is_an_arc_of p2,
p4 &
P c= closed_inside_of_rectangle a,
b,
c,
d &
Q c= closed_inside_of_rectangle a,
b,
c,
d holds
P meets Q
theorem Th88: :: JGRAPH_7:88
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `2 = d &
p3 `2 = d &
p4 `2 = d &
c <= p1 `2 &
p1 `2 <= d &
a <= p2 `1 &
p2 `1 < p3 `1 &
p3 `1 < p4 `1 &
p4 `1 <= b &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
rng f c= closed_inside_of_rectangle a,
b,
c,
d &
rng g c= closed_inside_of_rectangle a,
b,
c,
d holds
rng f meets rng g
theorem :: JGRAPH_7:89
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
P,
Q being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `2 = d &
p3 `2 = d &
p4 `2 = d &
c <= p1 `2 &
p1 `2 <= d &
a <= p2 `1 &
p2 `1 < p3 `1 &
p3 `1 < p4 `1 &
p4 `1 <= b &
P is_an_arc_of p1,
p3 &
Q is_an_arc_of p2,
p4 &
P c= closed_inside_of_rectangle a,
b,
c,
d &
Q c= closed_inside_of_rectangle a,
b,
c,
d holds
P meets Q
theorem Th90: :: JGRAPH_7:90
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `2 = d &
p3 `2 = d &
p4 `1 = b &
c <= p1 `2 &
p1 `2 <= d &
a <= p2 `1 &
p2 `1 < p3 `1 &
p3 `1 <= b &
c <= p4 `2 &
p4 `2 <= d &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
rng f c= closed_inside_of_rectangle a,
b,
c,
d &
rng g c= closed_inside_of_rectangle a,
b,
c,
d holds
rng f meets rng g
theorem :: JGRAPH_7:91
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
P,
Q being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `2 = d &
p3 `2 = d &
p4 `1 = b &
c <= p1 `2 &
p1 `2 <= d &
a <= p2 `1 &
p2 `1 < p3 `1 &
p3 `1 <= b &
c <= p4 `2 &
p4 `2 <= d &
P is_an_arc_of p1,
p3 &
Q is_an_arc_of p2,
p4 &
P c= closed_inside_of_rectangle a,
b,
c,
d &
Q c= closed_inside_of_rectangle a,
b,
c,
d holds
P meets Q
theorem Th92: :: JGRAPH_7:92
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `2 = d &
p3 `2 = d &
p4 `2 = c &
c <= p1 `2 &
p1 `2 <= d &
a <= p2 `1 &
p2 `1 < p3 `1 &
p3 `1 <= b &
a < p4 `1 &
p4 `1 <= b &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
rng f c= closed_inside_of_rectangle a,
b,
c,
d &
rng g c= closed_inside_of_rectangle a,
b,
c,
d holds
rng f meets rng g
theorem :: JGRAPH_7:93
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
P,
Q being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `2 = d &
p3 `2 = d &
p4 `2 = c &
c <= p1 `2 &
p1 `2 <= d &
a <= p2 `1 &
p2 `1 < p3 `1 &
p3 `1 <= b &
a < p4 `1 &
p4 `1 <= b &
P is_an_arc_of p1,
p3 &
Q is_an_arc_of p2,
p4 &
P c= closed_inside_of_rectangle a,
b,
c,
d &
Q c= closed_inside_of_rectangle a,
b,
c,
d holds
P meets Q
theorem Th94: :: JGRAPH_7:94
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `2 = d &
p3 `1 = b &
p4 `1 = b &
c <= p1 `2 &
p1 `2 <= d &
a <= p2 `1 &
p2 `1 <= b &
c <= p4 `2 &
p4 `2 < p3 `2 &
p3 `2 <= d &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
rng f c= closed_inside_of_rectangle a,
b,
c,
d &
rng g c= closed_inside_of_rectangle a,
b,
c,
d holds
rng f meets rng g
theorem :: JGRAPH_7:95
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
P,
Q being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `2 = d &
p3 `1 = b &
p4 `1 = b &
c <= p1 `2 &
p1 `2 <= d &
a <= p2 `1 &
p2 `1 <= b &
c <= p4 `2 &
p4 `2 < p3 `2 &
p3 `2 <= d &
P is_an_arc_of p1,
p3 &
Q is_an_arc_of p2,
p4 &
P c= closed_inside_of_rectangle a,
b,
c,
d &
Q c= closed_inside_of_rectangle a,
b,
c,
d holds
P meets Q
theorem Th96: :: JGRAPH_7:96
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `2 = d &
p3 `1 = b &
p4 `2 = c &
c <= p1 `2 &
p1 `2 <= d &
a <= p2 `1 &
p2 `1 <= b &
c <= p3 `2 &
p3 `2 <= d &
a < p4 `1 &
p4 `1 <= b &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
rng f c= closed_inside_of_rectangle a,
b,
c,
d &
rng g c= closed_inside_of_rectangle a,
b,
c,
d holds
rng f meets rng g
theorem :: JGRAPH_7:97
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
P,
Q being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `2 = d &
p3 `1 = b &
p4 `2 = c &
c <= p1 `2 &
p1 `2 <= d &
a <= p2 `1 &
p2 `1 <= b &
c <= p3 `2 &
p3 `2 <= d &
a < p4 `1 &
p4 `1 <= b &
P is_an_arc_of p1,
p3 &
Q is_an_arc_of p2,
p4 &
P c= closed_inside_of_rectangle a,
b,
c,
d &
Q c= closed_inside_of_rectangle a,
b,
c,
d holds
P meets Q
theorem Th98: :: JGRAPH_7:98
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `2 = d &
p3 `2 = c &
p4 `2 = c &
c <= p1 `2 &
p1 `2 <= d &
a <= p2 `1 &
p2 `1 <= b &
a < p4 `1 &
p4 `1 < p3 `1 &
p3 `1 <= b &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
rng f c= closed_inside_of_rectangle a,
b,
c,
d &
rng g c= closed_inside_of_rectangle a,
b,
c,
d holds
rng f meets rng g
theorem :: JGRAPH_7:99
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
P,
Q being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `2 = d &
p3 `2 = c &
p4 `2 = c &
c <= p1 `2 &
p1 `2 <= d &
a <= p2 `1 &
p2 `1 <= b &
a < p4 `1 &
p4 `1 < p3 `1 &
p3 `1 <= b &
P is_an_arc_of p1,
p3 &
Q is_an_arc_of p2,
p4 &
P c= closed_inside_of_rectangle a,
b,
c,
d &
Q c= closed_inside_of_rectangle a,
b,
c,
d holds
P meets Q
theorem Th100: :: JGRAPH_7:100
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `1 = b &
p3 `1 = b &
p4 `1 = b &
c <= p1 `2 &
p1 `2 <= d &
c <= p4 `2 &
p4 `2 < p3 `2 &
p3 `2 < p2 `2 &
p2 `2 <= d &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
rng f c= closed_inside_of_rectangle a,
b,
c,
d &
rng g c= closed_inside_of_rectangle a,
b,
c,
d holds
rng f meets rng g
theorem :: JGRAPH_7:101
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
P,
Q being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `1 = b &
p3 `1 = b &
p4 `1 = b &
c <= p1 `2 &
p1 `2 <= d &
c <= p4 `2 &
p4 `2 < p3 `2 &
p3 `2 < p2 `2 &
p2 `2 <= d &
P is_an_arc_of p1,
p3 &
Q is_an_arc_of p2,
p4 &
P c= closed_inside_of_rectangle a,
b,
c,
d &
Q c= closed_inside_of_rectangle a,
b,
c,
d holds
P meets Q
theorem Th102: :: JGRAPH_7:102
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `1 = b &
p3 `1 = b &
p4 `2 = c &
c <= p1 `2 &
p1 `2 <= d &
c <= p3 `2 &
p3 `2 < p2 `2 &
p2 `2 <= d &
a < p4 `1 &
p4 `1 <= b &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
rng f c= closed_inside_of_rectangle a,
b,
c,
d &
rng g c= closed_inside_of_rectangle a,
b,
c,
d holds
rng f meets rng g
theorem :: JGRAPH_7:103
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
P,
Q being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `1 = b &
p3 `1 = b &
p4 `2 = c &
c <= p1 `2 &
p1 `2 <= d &
c <= p3 `2 &
p3 `2 < p2 `2 &
p2 `2 <= d &
a < p4 `1 &
p4 `1 <= b &
P is_an_arc_of p1,
p3 &
Q is_an_arc_of p2,
p4 &
P c= closed_inside_of_rectangle a,
b,
c,
d &
Q c= closed_inside_of_rectangle a,
b,
c,
d holds
P meets Q
theorem Th104: :: JGRAPH_7:104
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `1 = b &
p3 `2 = c &
p4 `2 = c &
c <= p1 `2 &
p1 `2 <= d &
c <= p2 `2 &
p2 `2 <= d &
a < p4 `1 &
p4 `1 < p3 `1 &
p3 `1 <= b &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
rng f c= closed_inside_of_rectangle a,
b,
c,
d &
rng g c= closed_inside_of_rectangle a,
b,
c,
d holds
rng f meets rng g
theorem :: JGRAPH_7:105
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
P,
Q being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `1 = b &
p3 `2 = c &
p4 `2 = c &
c <= p1 `2 &
p1 `2 <= d &
c <= p2 `2 &
p2 `2 <= d &
a < p4 `1 &
p4 `1 < p3 `1 &
p3 `1 <= b &
P is_an_arc_of p1,
p3 &
Q is_an_arc_of p2,
p4 &
P c= closed_inside_of_rectangle a,
b,
c,
d &
Q c= closed_inside_of_rectangle a,
b,
c,
d holds
P meets Q
theorem Th106: :: JGRAPH_7:106
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `2 = c &
p3 `2 = c &
p4 `2 = c &
c <= p1 `2 &
p1 `2 <= d &
a < p4 `1 &
p4 `1 < p3 `1 &
p3 `1 < p2 `1 &
p2 `1 <= b &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
rng f c= closed_inside_of_rectangle a,
b,
c,
d &
rng g c= closed_inside_of_rectangle a,
b,
c,
d holds
rng f meets rng g
theorem :: JGRAPH_7:107
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
P,
Q being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = a &
p2 `2 = c &
p3 `2 = c &
p4 `2 = c &
c <= p1 `2 &
p1 `2 <= d &
a < p4 `1 &
p4 `1 < p3 `1 &
p3 `1 < p2 `1 &
p2 `1 <= b &
P is_an_arc_of p1,
p3 &
Q is_an_arc_of p2,
p4 &
P c= closed_inside_of_rectangle a,
b,
c,
d &
Q c= closed_inside_of_rectangle a,
b,
c,
d holds
P meets Q
theorem Th108: :: JGRAPH_7:108
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
a < b &
c < d &
p1 `2 = d &
p2 `2 = d &
p3 `2 = d &
p4 `2 = d &
a <= p1 `1 &
p1 `1 < p2 `1 &
p2 `1 < p3 `1 &
p3 `1 < p4 `1 &
p4 `1 <= b &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
rng f c= closed_inside_of_rectangle a,
b,
c,
d &
rng g c= closed_inside_of_rectangle a,
b,
c,
d holds
rng f meets rng g
theorem :: JGRAPH_7:109
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
P,
Q being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 `2 = d &
p2 `2 = d &
p3 `2 = d &
p4 `2 = d &
a <= p1 `1 &
p1 `1 < p2 `1 &
p2 `1 < p3 `1 &
p3 `1 < p4 `1 &
p4 `1 <= b &
P is_an_arc_of p1,
p3 &
Q is_an_arc_of p2,
p4 &
P c= closed_inside_of_rectangle a,
b,
c,
d &
Q c= closed_inside_of_rectangle a,
b,
c,
d holds
P meets Q
theorem Th110: :: JGRAPH_7:110
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
a < b &
c < d &
p1 `2 = d &
p2 `2 = d &
p3 `2 = d &
p4 `1 = b &
a <= p1 `1 &
p1 `1 < p2 `1 &
p2 `1 < p3 `1 &
p3 `1 <= b &
c <= p4 `2 &
p4 `2 <= d &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
rng f c= closed_inside_of_rectangle a,
b,
c,
d &
rng g c= closed_inside_of_rectangle a,
b,
c,
d holds
rng f meets rng g
theorem :: JGRAPH_7:111
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
P,
Q being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 `2 = d &
p2 `2 = d &
p3 `2 = d &
p4 `1 = b &
a <= p1 `1 &
p1 `1 < p2 `1 &
p2 `1 < p3 `1 &
p3 `1 <= b &
c <= p4 `2 &
p4 `2 <= d &
P is_an_arc_of p1,
p3 &
Q is_an_arc_of p2,
p4 &
P c= closed_inside_of_rectangle a,
b,
c,
d &
Q c= closed_inside_of_rectangle a,
b,
c,
d holds
P meets Q
theorem Th112: :: JGRAPH_7:112
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
a < b &
c < d &
p1 `2 = d &
p2 `2 = d &
p3 `2 = d &
p4 `2 = c &
a <= p1 `1 &
p1 `1 < p2 `1 &
p2 `1 < p3 `1 &
p3 `1 <= b &
a < p4 `1 &
p4 `1 <= b &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
rng f c= closed_inside_of_rectangle a,
b,
c,
d &
rng g c= closed_inside_of_rectangle a,
b,
c,
d holds
rng f meets rng g
theorem :: JGRAPH_7:113
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
P,
Q being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 `2 = d &
p2 `2 = d &
p3 `2 = d &
p4 `2 = c &
a <= p1 `1 &
p1 `1 < p2 `1 &
p2 `1 < p3 `1 &
p3 `1 <= b &
a < p4 `1 &
p4 `1 <= b &
P is_an_arc_of p1,
p3 &
Q is_an_arc_of p2,
p4 &
P c= closed_inside_of_rectangle a,
b,
c,
d &
Q c= closed_inside_of_rectangle a,
b,
c,
d holds
P meets Q
theorem Th114: :: JGRAPH_7:114
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
a < b &
c < d &
p1 `2 = d &
p2 `2 = d &
p3 `1 = b &
p4 `1 = b &
a <= p1 `1 &
p1 `1 < p2 `1 &
p2 `1 <= b &
c <= p4 `2 &
p4 `2 < p3 `2 &
p3 `2 <= d &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
rng f c= closed_inside_of_rectangle a,
b,
c,
d &
rng g c= closed_inside_of_rectangle a,
b,
c,
d holds
rng f meets rng g
theorem :: JGRAPH_7:115
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
P,
Q being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 `2 = d &
p2 `2 = d &
p3 `1 = b &
p4 `1 = b &
a <= p1 `1 &
p1 `1 < p2 `1 &
p2 `1 <= b &
c <= p4 `2 &
p4 `2 < p3 `2 &
p3 `2 <= d &
P is_an_arc_of p1,
p3 &
Q is_an_arc_of p2,
p4 &
P c= closed_inside_of_rectangle a,
b,
c,
d &
Q c= closed_inside_of_rectangle a,
b,
c,
d holds
P meets Q
theorem Th116: :: JGRAPH_7:116
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
a < b &
c < d &
p1 `2 = d &
p2 `2 = d &
p3 `1 = b &
p4 `2 = c &
a <= p1 `1 &
p1 `1 < p2 `1 &
p2 `1 <= b &
c <= p3 `2 &
p3 `2 <= d &
a < p4 `1 &
p4 `1 <= b &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
rng f c= closed_inside_of_rectangle a,
b,
c,
d &
rng g c= closed_inside_of_rectangle a,
b,
c,
d holds
rng f meets rng g
theorem :: JGRAPH_7:117
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
P,
Q being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 `2 = d &
p2 `2 = d &
p3 `1 = b &
p4 `2 = c &
a <= p1 `1 &
p1 `1 < p2 `1 &
p2 `1 <= b &
c <= p3 `2 &
p3 `2 <= d &
a < p4 `1 &
p4 `1 <= b &
P is_an_arc_of p1,
p3 &
Q is_an_arc_of p2,
p4 &
P c= closed_inside_of_rectangle a,
b,
c,
d &
Q c= closed_inside_of_rectangle a,
b,
c,
d holds
P meets Q
theorem Th118: :: JGRAPH_7:118
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
a < b &
c < d &
p1 `2 = d &
p2 `2 = d &
p3 `2 = c &
p4 `2 = c &
a <= p1 `1 &
p1 `1 < p2 `1 &
p2 `1 <= b &
a < p4 `1 &
p4 `1 < p3 `1 &
p3 `1 <= b &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
rng f c= closed_inside_of_rectangle a,
b,
c,
d &
rng g c= closed_inside_of_rectangle a,
b,
c,
d holds
rng f meets rng g
theorem :: JGRAPH_7:119
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
P,
Q being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 `2 = d &
p2 `2 = d &
p3 `2 = c &
p4 `2 = c &
a <= p1 `1 &
p1 `1 < p2 `1 &
p2 `1 <= b &
a < p4 `1 &
p4 `1 < p3 `1 &
p3 `1 <= b &
P is_an_arc_of p1,
p3 &
Q is_an_arc_of p2,
p4 &
P c= closed_inside_of_rectangle a,
b,
c,
d &
Q c= closed_inside_of_rectangle a,
b,
c,
d holds
P meets Q
theorem Th120: :: JGRAPH_7:120
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
a < b &
c < d &
p1 `2 = d &
p2 `1 = b &
p3 `1 = b &
p4 `1 = b &
a <= p1 `1 &
p1 `1 <= b &
d >= p2 `2 &
p2 `2 > p3 `2 &
p3 `2 > p4 `2 &
p4 `2 >= c &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
rng f c= closed_inside_of_rectangle a,
b,
c,
d &
rng g c= closed_inside_of_rectangle a,
b,
c,
d holds
rng f meets rng g
theorem :: JGRAPH_7:121
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
P,
Q being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 `2 = d &
p2 `1 = b &
p3 `1 = b &
p4 `1 = b &
a <= p1 `1 &
p1 `1 <= b &
d >= p2 `2 &
p2 `2 > p3 `2 &
p3 `2 > p4 `2 &
p4 `2 >= c &
P is_an_arc_of p1,
p3 &
Q is_an_arc_of p2,
p4 &
P c= closed_inside_of_rectangle a,
b,
c,
d &
Q c= closed_inside_of_rectangle a,
b,
c,
d holds
P meets Q
theorem Th122: :: JGRAPH_7:122
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
a < b &
c < d &
p1 `2 = d &
p2 `1 = b &
p3 `1 = b &
p4 `2 = c &
a <= p1 `1 &
p1 `1 <= b &
d >= p2 `2 &
p2 `2 > p3 `2 &
p3 `2 >= c &
a < p4 `1 &
p4 `1 <= b &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
rng f c= closed_inside_of_rectangle a,
b,
c,
d &
rng g c= closed_inside_of_rectangle a,
b,
c,
d holds
rng f meets rng g
theorem :: JGRAPH_7:123
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
P,
Q being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 `2 = d &
p2 `1 = b &
p3 `1 = b &
p4 `2 = c &
a <= p1 `1 &
p1 `1 <= b &
d >= p2 `2 &
p2 `2 > p3 `2 &
p3 `2 >= c &
a < p4 `1 &
p4 `1 <= b &
P is_an_arc_of p1,
p3 &
Q is_an_arc_of p2,
p4 &
P c= closed_inside_of_rectangle a,
b,
c,
d &
Q c= closed_inside_of_rectangle a,
b,
c,
d holds
P meets Q
theorem Th124: :: JGRAPH_7:124
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
a < b &
c < d &
p1 `2 = d &
p2 `1 = b &
p3 `2 = c &
p4 `2 = c &
a <= p1 `1 &
p1 `1 <= b &
c <= p2 `2 &
p2 `2 <= d &
a < p4 `1 &
p4 `1 < p3 `1 &
p3 `1 <= b &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
rng f c= closed_inside_of_rectangle a,
b,
c,
d &
rng g c= closed_inside_of_rectangle a,
b,
c,
d holds
rng f meets rng g
theorem :: JGRAPH_7:125
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
P,
Q being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 `2 = d &
p2 `1 = b &
p3 `2 = c &
p4 `2 = c &
a <= p1 `1 &
p1 `1 <= b &
c <= p2 `2 &
p2 `2 <= d &
a < p4 `1 &
p4 `1 < p3 `1 &
p3 `1 <= b &
P is_an_arc_of p1,
p3 &
Q is_an_arc_of p2,
p4 &
P c= closed_inside_of_rectangle a,
b,
c,
d &
Q c= closed_inside_of_rectangle a,
b,
c,
d holds
P meets Q
theorem Th126: :: JGRAPH_7:126
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
a < b &
c < d &
p1 `2 = d &
p2 `2 = c &
p3 `2 = c &
p4 `2 = c &
a <= p1 `1 &
p1 `1 <= b &
a < p4 `1 &
p4 `1 < p3 `1 &
p3 `1 < p2 `1 &
p2 `1 <= b &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
rng f c= closed_inside_of_rectangle a,
b,
c,
d &
rng g c= closed_inside_of_rectangle a,
b,
c,
d holds
rng f meets rng g
theorem :: JGRAPH_7:127
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
P,
Q being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 `2 = d &
p2 `2 = c &
p3 `2 = c &
p4 `2 = c &
a <= p1 `1 &
p1 `1 <= b &
a < p4 `1 &
p4 `1 < p3 `1 &
p3 `1 < p2 `1 &
p2 `1 <= b &
P is_an_arc_of p1,
p3 &
Q is_an_arc_of p2,
p4 &
P c= closed_inside_of_rectangle a,
b,
c,
d &
Q c= closed_inside_of_rectangle a,
b,
c,
d holds
P meets Q
theorem Th128: :: JGRAPH_7:128
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = b &
p2 `1 = b &
p3 `1 = b &
p4 `1 = b &
d >= p1 `2 &
p1 `2 > p2 `2 &
p2 `2 > p3 `2 &
p3 `2 > p4 `2 &
p4 `2 >= c &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
rng f c= closed_inside_of_rectangle a,
b,
c,
d &
rng g c= closed_inside_of_rectangle a,
b,
c,
d holds
rng f meets rng g
theorem :: JGRAPH_7:129
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
P,
Q being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = b &
p2 `1 = b &
p3 `1 = b &
p4 `1 = b &
d >= p1 `2 &
p1 `2 > p2 `2 &
p2 `2 > p3 `2 &
p3 `2 > p4 `2 &
p4 `2 >= c &
P is_an_arc_of p1,
p3 &
Q is_an_arc_of p2,
p4 &
P c= closed_inside_of_rectangle a,
b,
c,
d &
Q c= closed_inside_of_rectangle a,
b,
c,
d holds
P meets Q
theorem Th130: :: JGRAPH_7:130
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = b &
p2 `1 = b &
p3 `1 = b &
p4 `2 = c &
d >= p1 `2 &
p1 `2 > p2 `2 &
p2 `2 > p3 `2 &
p3 `2 >= c &
a < p4 `1 &
p4 `1 <= b &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
rng f c= closed_inside_of_rectangle a,
b,
c,
d &
rng g c= closed_inside_of_rectangle a,
b,
c,
d holds
rng f meets rng g
theorem :: JGRAPH_7:131
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
P,
Q being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = b &
p2 `1 = b &
p3 `1 = b &
p4 `2 = c &
d >= p1 `2 &
p1 `2 > p2 `2 &
p2 `2 > p3 `2 &
p3 `2 >= c &
a < p4 `1 &
p4 `1 <= b &
P is_an_arc_of p1,
p3 &
Q is_an_arc_of p2,
p4 &
P c= closed_inside_of_rectangle a,
b,
c,
d &
Q c= closed_inside_of_rectangle a,
b,
c,
d holds
P meets Q
theorem Th132: :: JGRAPH_7:132
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = b &
p2 `1 = b &
p3 `2 = c &
p4 `2 = c &
d >= p1 `2 &
p1 `2 > p2 `2 &
p2 `2 >= c &
b >= p3 `1 &
p3 `1 > p4 `1 &
p4 `1 > a &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
rng f c= closed_inside_of_rectangle a,
b,
c,
d &
rng g c= closed_inside_of_rectangle a,
b,
c,
d holds
rng f meets rng g
theorem :: JGRAPH_7:133
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
P,
Q being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = b &
p2 `1 = b &
p3 `2 = c &
p4 `2 = c &
d >= p1 `2 &
p1 `2 > p2 `2 &
p2 `2 >= c &
b >= p3 `1 &
p3 `1 > p4 `1 &
p4 `1 > a &
P is_an_arc_of p1,
p3 &
Q is_an_arc_of p2,
p4 &
P c= closed_inside_of_rectangle a,
b,
c,
d &
Q c= closed_inside_of_rectangle a,
b,
c,
d holds
P meets Q
theorem Th134: :: JGRAPH_7:134
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = b &
p2 `2 = c &
p3 `2 = c &
p4 `2 = c &
c <= p1 `2 &
p1 `2 <= d &
b >= p2 `1 &
p2 `1 > p3 `1 &
p3 `1 > p4 `1 &
p4 `1 > a &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
rng f c= closed_inside_of_rectangle a,
b,
c,
d &
rng g c= closed_inside_of_rectangle a,
b,
c,
d holds
rng f meets rng g
theorem :: JGRAPH_7:135
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
P,
Q being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 `1 = b &
p2 `2 = c &
p3 `2 = c &
p4 `2 = c &
c <= p1 `2 &
p1 `2 <= d &
b >= p2 `1 &
p2 `1 > p3 `1 &
p3 `1 > p4 `1 &
p4 `1 > a &
P is_an_arc_of p1,
p3 &
Q is_an_arc_of p2,
p4 &
P c= closed_inside_of_rectangle a,
b,
c,
d &
Q c= closed_inside_of_rectangle a,
b,
c,
d holds
P meets Q
theorem Th136: :: JGRAPH_7:136
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
f,
g being
Function of
I[01] ,
(TOP-REAL 2) st
a < b &
c < d &
p1 `2 = c &
p2 `2 = c &
p3 `2 = c &
p4 `2 = c &
b >= p1 `1 &
p1 `1 > p2 `1 &
p2 `1 > p3 `1 &
p3 `1 > p4 `1 &
p4 `1 > a &
f . 0 = p1 &
f . 1
= p3 &
g . 0 = p2 &
g . 1
= p4 &
f is
continuous &
f is
one-to-one &
g is
continuous &
g is
one-to-one &
rng f c= closed_inside_of_rectangle a,
b,
c,
d &
rng g c= closed_inside_of_rectangle a,
b,
c,
d holds
rng f meets rng g
theorem :: JGRAPH_7:137
for
p1,
p2,
p3,
p4 being
Point of
(TOP-REAL 2) for
a,
b,
c,
d being
real number for
P,
Q being
Subset of
(TOP-REAL 2) st
a < b &
c < d &
p1 `2 = c &
p2 `2 = c &
p3 `2 = c &
p4 `2 = c &
b >= p1 `1 &
p1 `1 > p2 `1 &
p2 `1 > p3 `1 &
p3 `1 > p4 `1 &
p4 `1 > a &
P is_an_arc_of p1,
p3 &
Q is_an_arc_of p2,
p4 &
P c= closed_inside_of_rectangle a,
b,
c,
d &
Q c= closed_inside_of_rectangle a,
b,
c,
d holds
P meets Q