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