:: Fashoda Meet Theorem for Rectangles
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Copyright (c) 2005-2021 Association of Mizar Users

theorem Th1: :: JGRAPH_7:1
for a, b, d being Real
for p being Point of () st a < b & p 2 = d & a <= p 1 & p 1 <= b holds
p in LSeg (|[a,d]|,|[b,d]|)
proof end;

theorem Th2: :: JGRAPH_7:2
for n being Element of NAT
for P being Subset of ()
for p1, p2 being Point of () st P is_an_arc_of p1,p2 holds
ex f being Function of I[01],() st
( f is continuous & f is one-to-one & rng f = P & f . 0 = p1 & f . 1 = p2 )
proof end;

theorem Th3: :: JGRAPH_7:3
for p1, p2 being Point of ()
for b, c, d being Real st p1 1 < b & p1 1 = p2 1 & c <= p1 2 & p1 2 < p2 2 & p2 2 <= d holds
LE p1,p2, rectangle ((p1 1),b,c,d)
proof end;

theorem Th4: :: JGRAPH_7:4
for p1, p2 being Point of ()
for b, c being Real st p1 1 < b & c < p2 2 & c <= p1 2 & p1 2 <= p2 2 & p1 1 <= p2 1 & p2 1 <= b holds
LE p1,p2, rectangle ((p1 1),b,c,(p2 2))
proof end;

theorem Th5: :: JGRAPH_7:5
for p1, p2 being Point of ()
for c, d being Real st p1 1 < p2 1 & c < d & c <= p1 2 & p1 2 <= d & c <= p2 2 & p2 2 <= d holds
LE p1,p2, rectangle ((p1 1),(p2 1),c,d)
proof end;

theorem Th6: :: JGRAPH_7:6
for p1, p2 being Point of ()
for b, d being Real st p2 2 < d & p2 2 <= p1 2 & p1 2 <= d & p1 1 < p2 1 & p2 1 <= b holds
LE p1,p2, rectangle ((p1 1),b,(p2 2),d)
proof end;

theorem Th7: :: JGRAPH_7:7
for p1, p2 being Point of ()
for a, b, c, d being Real st a < b & c < d & p1 2 = d & p2 2 = d & a <= p1 1 & p1 1 < p2 1 & p2 1 <= b holds
LE p1,p2, rectangle (a,b,c,d)
proof end;

theorem Th8: :: JGRAPH_7:8
for p1, p2 being Point of ()
for a, b, c, d being Real st a < b & c < d & p1 2 = d & p2 1 = b & a <= p1 1 & p1 1 <= b & c <= p2 2 & p2 2 <= d holds
LE p1,p2, rectangle (a,b,c,d)
proof end;

theorem Th9: :: JGRAPH_7:9
for p1, p2 being Point of ()
for a, b, c, d being Real st a < b & c < d & p1 2 = d & p2 2 = c & a <= p1 1 & p1 1 <= b & a < p2 1 & p2 1 <= b holds
LE p1,p2, rectangle (a,b,c,d)
proof end;

theorem Th10: :: JGRAPH_7:10
for p1, p2 being Point of ()
for a, b, c, d being Real st a < b & c < d & p1 1 = b & p2 1 = b & c <= p2 2 & p2 2 < p1 2 & p1 2 <= d holds
LE p1,p2, rectangle (a,b,c,d)
proof end;

theorem Th11: :: JGRAPH_7:11
for p1, p2 being Point of ()
for a, b, c, d being Real st a < b & c < d & p1 1 = b & p2 2 = c & c <= p1 2 & p1 2 <= d & a < p2 1 & p2 1 <= b holds
LE p1,p2, rectangle (a,b,c,d)
proof end;

theorem Th12: :: JGRAPH_7:12
for p1, p2 being Point of ()
for a, b, c, d being Real st a < b & c < d & p1 2 = c & p2 2 = c & a < p2 1 & p2 1 < p1 1 & p1 1 <= b holds
LE p1,p2, rectangle (a,b,c,d)
proof end;

theorem Th13: :: JGRAPH_7:13
for p1, p2 being Point of ()
for a, b, c, d being Real st a < b & c < d & p1 2 = d & p2 1 = b & a <= p1 1 & p1 1 <= b & c <= p2 2 & p2 2 <= d holds
LE p1,p2, rectangle (a,b,c,d)
proof end;

theorem Th14: :: JGRAPH_7:14
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real 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)
proof end;

theorem Th15: :: JGRAPH_7:15
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real 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)
proof end;

theorem Th16: :: JGRAPH_7:16
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real 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)
proof end;

theorem Th17: :: JGRAPH_7:17
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real 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)
proof end;

theorem Th18: :: JGRAPH_7:18
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real 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)
proof end;

theorem Th19: :: JGRAPH_7:19
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real 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)
proof end;

theorem Th20: :: JGRAPH_7:20
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real 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)
proof end;

theorem Th21: :: JGRAPH_7:21
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real 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)
proof end;

theorem Th22: :: JGRAPH_7:22
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real 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)
proof end;

theorem Th23: :: JGRAPH_7:23
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real 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)
proof end;

theorem Th24: :: JGRAPH_7:24
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real 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)
proof end;

theorem Th25: :: JGRAPH_7:25
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real 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)
proof end;

theorem Th26: :: JGRAPH_7:26
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real 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)
proof end;

theorem Th27: :: JGRAPH_7:27
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real 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)
proof end;

theorem Th28: :: JGRAPH_7:28
for p1, p2, p3, p4 being Point of () st p1 1 <> p3 1 & p4 2 <> p2 2 & p4 2 <= p1 2 & p1 2 <= p2 2 & p1 1 <= p2 1 & p2 1 <= p3 1 & p4 2 <= p3 2 & p3 2 <= p2 2 & p1 1 < p4 1 & p4 1 <= p3 1 holds
p1,p2,p3,p4 are_in_this_order_on rectangle ((p1 1),(p3 1),(p4 2),(p2 2))
proof end;

theorem Th29: :: JGRAPH_7:29
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real 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)
proof end;

theorem Th30: :: JGRAPH_7:30
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real 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)
proof end;

theorem Th31: :: JGRAPH_7:31
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real 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)
proof end;

theorem Th32: :: JGRAPH_7:32
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real 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)
proof end;

theorem Th33: :: JGRAPH_7:33
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real 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)
proof end;

theorem Th34: :: JGRAPH_7:34
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real 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)
proof end;

theorem Th35: :: JGRAPH_7:35
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real 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)
proof end;

theorem Th36: :: JGRAPH_7:36
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real 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)
proof end;

theorem Th37: :: JGRAPH_7:37
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real 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)
proof end;

theorem Th38: :: JGRAPH_7:38
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real 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)
proof end;

theorem Th39: :: JGRAPH_7:39
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real 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)
proof end;

theorem Th40: :: JGRAPH_7:40
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real 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)
proof end;

theorem Th41: :: JGRAPH_7:41
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real 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)
proof end;

theorem Th42: :: JGRAPH_7:42
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real 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)
proof end;

theorem Th43: :: JGRAPH_7:43
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real 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)
proof end;

theorem Th44: :: JGRAPH_7:44
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real 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)
proof end;

theorem Th45: :: JGRAPH_7:45
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real 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)
proof end;

theorem Th46: :: JGRAPH_7:46
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real 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)
proof end;

theorem Th47: :: JGRAPH_7:47
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real 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)
proof end;

theorem Th48: :: JGRAPH_7:48
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real 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)
proof end;

theorem Th49: :: JGRAPH_7:49
for A, B, C, D being Real
for h, g being Function of (),() 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 " )
proof end;

theorem Th50: :: JGRAPH_7:50
for A, B, C, D being Real
for h being Function of (),() st A > 0 & C > 0 & h = AffineMap (A,B,C,D) holds
( h is being_homeomorphism & ( for p1, p2 being Point of () st p1 1 < p2 1 holds
(h . p1) 1 < (h . p2) 1 ) )
proof end;

theorem Th51: :: JGRAPH_7:51
for A, B, C, D being Real
for h being Function of (),() st A > 0 & C > 0 & h = AffineMap (A,B,C,D) holds
( h is being_homeomorphism & ( for p1, p2 being Point of () st p1 2 < p2 2 holds
(h . p1) 2 < (h . p2) 2 ) )
proof end;

theorem Th52: :: JGRAPH_7:52
for a, b, c, d being Real
for h being Function of (),()
for f being Function of I[01],() 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)
proof end;

theorem Th53: :: JGRAPH_7:53
for a, b, c, d being Real
for h being Function of (),()
for f being Function of I[01],() st a < b & c < d & h = AffineMap ((2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) & f is continuous & f is one-to-one holds
( h * f is continuous & h * f is one-to-one )
proof end;

theorem Th54: :: JGRAPH_7:54
for a, b, c, d being Real
for h being Function of (),()
for f being Function of I[01],()
for O being Point of I[01] st a < b & h = AffineMap ((2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) & (f . O) 1 = a holds
((h * f) . O) 1 = - 1
proof end;

theorem Th55: :: JGRAPH_7:55
for a, b, c, d being Real
for h being Function of (),()
for f being Function of I[01],()
for I being Point of I[01] st c < d & h = AffineMap ((2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) & (f . I) 2 = d holds
((h * f) . I) 2 = 1
proof end;

theorem Th56: :: JGRAPH_7:56
for a, b, c, d being Real
for h being Function of (),()
for f being Function of I[01],()
for I being Point of I[01] st a < b & h = AffineMap ((2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) & (f . I) 1 = b holds
((h * f) . I) 1 = 1
proof end;

theorem Th57: :: JGRAPH_7:57
for a, b, c, d being Real
for h being Function of (),()
for f being Function of I[01],()
for I being Point of I[01] st c < d & h = AffineMap ((2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) & (f . I) 2 = c holds
((h * f) . I) 2 = - 1
proof end;

theorem Th58: :: JGRAPH_7:58
for a, b, c, d being Real
for h being Function of (),()
for f being Function of I[01],()
for O, I being Point of I[01] st c < d & h = AffineMap ((2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) & c <= (f . O) 2 & (f . O) 2 < (f . I) 2 & (f . I) 2 <= d holds
( - 1 <= ((h * f) . O) 2 & ((h * f) . O) 2 < ((h * f) . I) 2 & ((h * f) . I) 2 <= 1 )
proof end;

theorem Th59: :: JGRAPH_7:59
for a, b, c, d being Real
for h being Function of (),()
for f being Function of I[01],()
for O, I being Point of I[01] st a < b & c < d & h = AffineMap ((2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) & c <= (f . O) 2 & (f . O) 2 <= d & a <= (f . I) 1 & (f . I) 1 <= b holds
( - 1 <= ((h * f) . O) 2 & ((h * f) . O) 2 <= 1 & - 1 <= ((h * f) . I) 1 & ((h * f) . I) 1 <= 1 )
proof end;

theorem Th60: :: JGRAPH_7:60
for a, b, c, d being Real
for h being Function of (),()
for f being Function of I[01],()
for O, I being Point of I[01] st c < d & h = AffineMap ((2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) & c <= (f . O) 2 & (f . O) 2 <= d & c <= (f . I) 2 & (f . I) 2 <= d holds
( - 1 <= ((h * f) . O) 2 & ((h * f) . O) 2 <= 1 & - 1 <= ((h * f) . I) 2 & ((h * f) . I) 2 <= 1 )
proof end;

theorem Th61: :: JGRAPH_7:61
for a, b, c, d being Real
for h being Function of (),()
for f being Function of I[01],()
for O, I being Point of I[01] st a < b & c < d & h = AffineMap ((2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) & c <= (f . O) 2 & (f . O) 2 <= d & a < (f . I) 1 & (f . I) 1 <= b holds
( - 1 <= ((h * f) . O) 2 & ((h * f) . O) 2 <= 1 & - 1 < ((h * f) . I) 1 & ((h * f) . I) 1 <= 1 )
proof end;

theorem Th62: :: JGRAPH_7:62
for a, b, c, d being Real
for h being Function of (),()
for f being Function of I[01],()
for O, I being Point of I[01] st a < b & h = AffineMap ((2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) & a <= (f . O) 1 & (f . O) 1 < (f . I) 1 & (f . I) 1 <= b holds
( - 1 <= ((h * f) . O) 1 & ((h * f) . O) 1 < ((h * f) . I) 1 & ((h * f) . I) 1 <= 1 )
proof end;

theorem Th63: :: JGRAPH_7:63
for a, b, c, d being Real
for h being Function of (),()
for f being Function of I[01],()
for O, I being Point of I[01] st a < b & c < d & h = AffineMap ((2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) & a <= (f . O) 1 & (f . O) 1 <= b & c <= (f . I) 2 & (f . I) 2 <= d holds
( - 1 <= ((h * f) . O) 1 & ((h * f) . O) 1 <= 1 & - 1 <= ((h * f) . I) 2 & ((h * f) . I) 2 <= 1 )
proof end;

theorem Th64: :: JGRAPH_7:64
for a, b, c, d being Real
for h being Function of (),()
for f being Function of I[01],()
for O, I being Point of I[01] st a < b & h = AffineMap ((2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) & a <= (f . O) 1 & (f . O) 1 <= b & a < (f . I) 1 & (f . I) 1 <= b holds
( - 1 <= ((h * f) . O) 1 & ((h * f) . O) 1 <= 1 & - 1 < ((h * f) . I) 1 & ((h * f) . I) 1 <= 1 )
proof end;

theorem Th65: :: JGRAPH_7:65
for a, b, c, d being Real
for h being Function of (),()
for f being Function of I[01],()
for O, I being Point of I[01] st c < d & h = AffineMap ((2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) & d >= (f . O) 2 & (f . O) 2 > (f . I) 2 & (f . I) 2 >= c holds
( 1 >= ((h * f) . O) 2 & ((h * f) . O) 2 > ((h * f) . I) 2 & ((h * f) . I) 2 >= - 1 )
proof end;

theorem Th66: :: JGRAPH_7:66
for a, b, c, d being Real
for h being Function of (),()
for f being Function of I[01],()
for O, I being Point of I[01] st a < b & c < d & h = AffineMap ((2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) & c <= (f . O) 2 & (f . O) 2 <= d & a < (f . I) 1 & (f . I) 1 <= b holds
( - 1 <= ((h * f) . O) 2 & ((h * f) . O) 2 <= 1 & - 1 < ((h * f) . I) 1 & ((h * f) . I) 1 <= 1 )
proof end;

theorem Th67: :: JGRAPH_7:67
for a, b, c, d being Real
for h being Function of (),()
for f being Function of I[01],()
for O, I being Point of I[01] st a < b & h = AffineMap ((2 / (b - a)),(- ((b + a) / (b - a))),(2 / (d - c)),(- ((d + c) / (d - c)))) & a < (f . I) 1 & (f . I) 1 < (f . O) 1 & (f . O) 1 <= b holds
( - 1 < ((h * f) . I) 1 & ((h * f) . I) 1 < ((h * f) . O) 1 & ((h * f) . O) 1 <= 1 )
proof end;

theorem Th68: :: JGRAPH_7:68
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
for f, g being Function of I[01],() 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
proof end;

theorem :: JGRAPH_7:69
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
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
proof end;

theorem Th70: :: JGRAPH_7:70
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
for f, g being Function of I[01],() 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
proof end;

theorem :: JGRAPH_7:71
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
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
proof end;

theorem Th72: :: JGRAPH_7:72
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
for f, g being Function of I[01],() 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
proof end;

theorem :: JGRAPH_7:73
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
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
proof end;

theorem Th74: :: JGRAPH_7:74
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
for f, g being Function of I[01],() 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
proof end;

theorem :: JGRAPH_7:75
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
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
proof end;

theorem Th76: :: JGRAPH_7:76
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
for f, g being Function of I[01],() 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
proof end;

theorem :: JGRAPH_7:77
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
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
proof end;

theorem Th78: :: JGRAPH_7:78
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
for f, g being Function of I[01],() 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
proof end;

theorem :: JGRAPH_7:79
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
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
proof end;

theorem Th80: :: JGRAPH_7:80
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
for f, g being Function of I[01],() 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
proof end;

theorem :: JGRAPH_7:81
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
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
proof end;

theorem Th82: :: JGRAPH_7:82
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
for f, g being Function of I[01],() 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
proof end;

theorem :: JGRAPH_7:83
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
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
proof end;

theorem Th84: :: JGRAPH_7:84
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
for f, g being Function of I[01],() 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
proof end;

theorem :: JGRAPH_7:85
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
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
proof end;

theorem Th86: :: JGRAPH_7:86
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
for f, g being Function of I[01],() 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
proof end;

theorem :: JGRAPH_7:87
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
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
proof end;

theorem Th88: :: JGRAPH_7:88
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
for f, g being Function of I[01],() 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
proof end;

theorem :: JGRAPH_7:89
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
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
proof end;

theorem Th90: :: JGRAPH_7:90
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
for f, g being Function of I[01],() 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
proof end;

theorem :: JGRAPH_7:91
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
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
proof end;

theorem Th92: :: JGRAPH_7:92
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
for f, g being Function of I[01],() 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
proof end;

theorem :: JGRAPH_7:93
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
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
proof end;

theorem Th94: :: JGRAPH_7:94
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
for f, g being Function of I[01],() 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
proof end;

theorem :: JGRAPH_7:95
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
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
proof end;

theorem Th96: :: JGRAPH_7:96
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
for f, g being Function of I[01],() 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
proof end;

theorem :: JGRAPH_7:97
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
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
proof end;

theorem Th98: :: JGRAPH_7:98
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
for f, g being Function of I[01],() 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
proof end;

theorem :: JGRAPH_7:99
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
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
proof end;

theorem Th100: :: JGRAPH_7:100
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
for f, g being Function of I[01],() 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
proof end;

theorem :: JGRAPH_7:101
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
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
proof end;

theorem Th102: :: JGRAPH_7:102
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
for f, g being Function of I[01],() 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
proof end;

theorem :: JGRAPH_7:103
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
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
proof end;

theorem Th104: :: JGRAPH_7:104
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
for f, g being Function of I[01],() 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
proof end;

theorem :: JGRAPH_7:105
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
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
proof end;

theorem Th106: :: JGRAPH_7:106
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
for f, g being Function of I[01],() 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
proof end;

theorem :: JGRAPH_7:107
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
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
proof end;

theorem Th108: :: JGRAPH_7:108
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
for f, g being Function of I[01],() 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
proof end;

theorem :: JGRAPH_7:109
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
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
proof end;

theorem Th110: :: JGRAPH_7:110
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
for f, g being Function of I[01],() 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
proof end;

theorem :: JGRAPH_7:111
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
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
proof end;

theorem Th112: :: JGRAPH_7:112
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
for f, g being Function of I[01],() 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
proof end;

theorem :: JGRAPH_7:113
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
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
proof end;

theorem Th114: :: JGRAPH_7:114
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
for f, g being Function of I[01],() 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
proof end;

theorem :: JGRAPH_7:115
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
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
proof end;

theorem Th116: :: JGRAPH_7:116
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
for f, g being Function of I[01],() 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
proof end;

theorem :: JGRAPH_7:117
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
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
proof end;

theorem Th118: :: JGRAPH_7:118
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
for f, g being Function of I[01],() 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
proof end;

theorem :: JGRAPH_7:119
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
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
proof end;

theorem Th120: :: JGRAPH_7:120
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
for f, g being Function of I[01],() 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
proof end;

theorem :: JGRAPH_7:121
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
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
proof end;

theorem Th122: :: JGRAPH_7:122
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
for f, g being Function of I[01],() 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
proof end;

theorem :: JGRAPH_7:123
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
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
proof end;

theorem Th124: :: JGRAPH_7:124
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
for f, g being Function of I[01],() 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
proof end;

theorem :: JGRAPH_7:125
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
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
proof end;

theorem Th126: :: JGRAPH_7:126
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
for f, g being Function of I[01],() 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
proof end;

theorem :: JGRAPH_7:127
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
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
proof end;

theorem Th128: :: JGRAPH_7:128
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
for f, g being Function of I[01],() 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
proof end;

theorem :: JGRAPH_7:129
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
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
proof end;

theorem Th130: :: JGRAPH_7:130
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
for f, g being Function of I[01],() 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
proof end;

theorem :: JGRAPH_7:131
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
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
proof end;

theorem Th132: :: JGRAPH_7:132
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
for f, g being Function of I[01],() 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
proof end;

theorem :: JGRAPH_7:133
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
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
proof end;

theorem Th134: :: JGRAPH_7:134
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
for f, g being Function of I[01],() 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
proof end;

theorem :: JGRAPH_7:135
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
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
proof end;

theorem Th136: :: JGRAPH_7:136
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
for f, g being Function of I[01],() 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
proof end;

theorem :: JGRAPH_7:137
for p1, p2, p3, p4 being Point of ()
for a, b, c, d being Real
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
proof end;