begin
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
for
p1,
p2,
p3,
p4 being
Point of
for
a,
b,
c,
d being
real number st
a < b &
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:
for
p1,
p2,
p3,
p4 being
Point of
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:
for
p1,
p2,
p3,
p4 being
Point of
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:
for
p1,
p2,
p3,
p4 being
Point of
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:
for
p1,
p2,
p3,
p4 being
Point of
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:
for
p1,
p2,
p3,
p4 being
Point of
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:
for
p1,
p2,
p3,
p4 being
Point of
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:
for
p1,
p2,
p3,
p4 being
Point of
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:
for
p1,
p2,
p3,
p4 being
Point of
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:
for
p1,
p2,
p3,
p4 being
Point of
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:
for
p1,
p2,
p3,
p4 being
Point of
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:
for
p1,
p2,
p3,
p4 being
Point of
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:
for
p1,
p2,
p3,
p4 being
Point of
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:
for
p1,
p2,
p3,
p4 being
Point of
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:
theorem Th29:
for
p1,
p2,
p3,
p4 being
Point of
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:
for
p1,
p2,
p3,
p4 being
Point of
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:
for
p1,
p2,
p3,
p4 being
Point of
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:
for
p1,
p2,
p3,
p4 being
Point of
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:
for
p1,
p2,
p3,
p4 being
Point of
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:
for
p1,
p2,
p3,
p4 being
Point of
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:
for
p1,
p2,
p3,
p4 being
Point of
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:
for
p1,
p2,
p3,
p4 being
Point of
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:
for
p1,
p2,
p3,
p4 being
Point of
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:
for
p1,
p2,
p3,
p4 being
Point of
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:
for
p1,
p2,
p3,
p4 being
Point of
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:
for
p1,
p2,
p3,
p4 being
Point of
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:
for
p1,
p2,
p3,
p4 being
Point of
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:
for
p1,
p2,
p3,
p4 being
Point of
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:
for
p1,
p2,
p3,
p4 being
Point of
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:
for
p1,
p2,
p3,
p4 being
Point of
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:
for
p1,
p2,
p3,
p4 being
Point of
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:
for
p1,
p2,
p3,
p4 being
Point of
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:
for
p1,
p2,
p3,
p4 being
Point of
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:
for
p1,
p2,
p3,
p4 being
Point of
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:
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:
theorem Th51:
theorem Th52:
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:
theorem Th54:
theorem Th55:
theorem Th56:
theorem Th57:
theorem Th58:
theorem Th59:
theorem Th60:
theorem Th61:
theorem Th62:
theorem Th63:
theorem Th64:
theorem Th65:
theorem Th66:
theorem Th67:
theorem Th68:
for
p1,
p2,
p3,
p4 being
Point of
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
for
p1,
p2,
p3,
p4 being
Point of
for
a,
b,
c,
d being
real number for
P,
Q being
Subset of 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:
for
p1,
p2,
p3,
p4 being
Point of
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
for
p1,
p2,
p3,
p4 being
Point of
for
a,
b,
c,
d being
real number for
P,
Q being
Subset of 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:
for
p1,
p2,
p3,
p4 being
Point of
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
for
p1,
p2,
p3,
p4 being
Point of
for
a,
b,
c,
d being
real number for
P,
Q being
Subset of 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:
for
p1,
p2,
p3,
p4 being
Point of
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
for
p1,
p2,
p3,
p4 being
Point of
for
a,
b,
c,
d being
real number for
P,
Q being
Subset of 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:
for
p1,
p2,
p3,
p4 being
Point of
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
for
p1,
p2,
p3,
p4 being
Point of
for
a,
b,
c,
d being
real number for
P,
Q being
Subset of 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:
for
p1,
p2,
p3,
p4 being
Point of
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
for
p1,
p2,
p3,
p4 being
Point of
for
a,
b,
c,
d being
real number for
P,
Q being
Subset of 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:
for
p1,
p2,
p3,
p4 being
Point of
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
for
p1,
p2,
p3,
p4 being
Point of
for
a,
b,
c,
d being
real number for
P,
Q being
Subset of 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:
for
p1,
p2,
p3,
p4 being
Point of
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
for
p1,
p2,
p3,
p4 being
Point of
for
a,
b,
c,
d being
real number for
P,
Q being
Subset of 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:
for
p1,
p2,
p3,
p4 being
Point of
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
for
p1,
p2,
p3,
p4 being
Point of
for
a,
b,
c,
d being
real number for
P,
Q being
Subset of 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:
for
p1,
p2,
p3,
p4 being
Point of
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
for
p1,
p2,
p3,
p4 being
Point of
for
a,
b,
c,
d being
real number for
P,
Q being
Subset of 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:
for
p1,
p2,
p3,
p4 being
Point of
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
for
p1,
p2,
p3,
p4 being
Point of
for
a,
b,
c,
d being
real number for
P,
Q being
Subset of 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:
for
p1,
p2,
p3,
p4 being
Point of
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
for
p1,
p2,
p3,
p4 being
Point of
for
a,
b,
c,
d being
real number for
P,
Q being
Subset of 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:
for
p1,
p2,
p3,
p4 being
Point of
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
for
p1,
p2,
p3,
p4 being
Point of
for
a,
b,
c,
d being
real number for
P,
Q being
Subset of 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:
for
p1,
p2,
p3,
p4 being
Point of
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
for
p1,
p2,
p3,
p4 being
Point of
for
a,
b,
c,
d being
real number for
P,
Q being
Subset of 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:
for
p1,
p2,
p3,
p4 being
Point of
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
for
p1,
p2,
p3,
p4 being
Point of
for
a,
b,
c,
d being
real number for
P,
Q being
Subset of 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:
for
p1,
p2,
p3,
p4 being
Point of
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
for
p1,
p2,
p3,
p4 being
Point of
for
a,
b,
c,
d being
real number for
P,
Q being
Subset of 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:
for
p1,
p2,
p3,
p4 being
Point of
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
for
p1,
p2,
p3,
p4 being
Point of
for
a,
b,
c,
d being
real number for
P,
Q being
Subset of 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:
for
p1,
p2,
p3,
p4 being
Point of
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
for
p1,
p2,
p3,
p4 being
Point of
for
a,
b,
c,
d being
real number for
P,
Q being
Subset of 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:
for
p1,
p2,
p3,
p4 being
Point of
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
for
p1,
p2,
p3,
p4 being
Point of
for
a,
b,
c,
d being
real number for
P,
Q being
Subset of 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:
for
p1,
p2,
p3,
p4 being
Point of
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
for
p1,
p2,
p3,
p4 being
Point of
for
a,
b,
c,
d being
real number for
P,
Q being
Subset of 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:
for
p1,
p2,
p3,
p4 being
Point of
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
for
p1,
p2,
p3,
p4 being
Point of
for
a,
b,
c,
d being
real number for
P,
Q being
Subset of 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:
for
p1,
p2,
p3,
p4 being
Point of
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
for
p1,
p2,
p3,
p4 being
Point of
for
a,
b,
c,
d being
real number for
P,
Q being
Subset of 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:
for
p1,
p2,
p3,
p4 being
Point of
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
for
p1,
p2,
p3,
p4 being
Point of
for
a,
b,
c,
d being
real number for
P,
Q being
Subset of 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:
for
p1,
p2,
p3,
p4 being
Point of
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
for
p1,
p2,
p3,
p4 being
Point of
for
a,
b,
c,
d being
real number for
P,
Q being
Subset of 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:
for
p1,
p2,
p3,
p4 being
Point of
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
for
p1,
p2,
p3,
p4 being
Point of
for
a,
b,
c,
d being
real number for
P,
Q being
Subset of 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:
for
p1,
p2,
p3,
p4 being
Point of
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
for
p1,
p2,
p3,
p4 being
Point of
for
a,
b,
c,
d being
real number for
P,
Q being
Subset of 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:
for
p1,
p2,
p3,
p4 being
Point of
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
for
p1,
p2,
p3,
p4 being
Point of
for
a,
b,
c,
d being
real number for
P,
Q being
Subset of 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:
for
p1,
p2,
p3,
p4 being
Point of
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
for
p1,
p2,
p3,
p4 being
Point of
for
a,
b,
c,
d being
real number for
P,
Q being
Subset of 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:
for
p1,
p2,
p3,
p4 being
Point of
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
for
p1,
p2,
p3,
p4 being
Point of
for
a,
b,
c,
d being
real number for
P,
Q being
Subset of 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:
for
p1,
p2,
p3,
p4 being
Point of
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
for
p1,
p2,
p3,
p4 being
Point of
for
a,
b,
c,
d being
real number for
P,
Q being
Subset of 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:
for
p1,
p2,
p3,
p4 being
Point of
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
for
p1,
p2,
p3,
p4 being
Point of
for
a,
b,
c,
d being
real number for
P,
Q being
Subset of 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:
for
p1,
p2,
p3,
p4 being
Point of
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
for
p1,
p2,
p3,
p4 being
Point of
for
a,
b,
c,
d being
real number for
P,
Q being
Subset of 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:
for
p1,
p2,
p3,
p4 being
Point of
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
for
p1,
p2,
p3,
p4 being
Point of
for
a,
b,
c,
d being
real number for
P,
Q being
Subset of 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:
for
p1,
p2,
p3,
p4 being
Point of
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
for
p1,
p2,
p3,
p4 being
Point of
for
a,
b,
c,
d being
real number for
P,
Q being
Subset of 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:
for
p1,
p2,
p3,
p4 being
Point of
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
for
p1,
p2,
p3,
p4 being
Point of
for
a,
b,
c,
d being
real number for
P,
Q being
Subset of 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