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

theorem Th1: :: JGRAPH_7:1

for a, b, d being Real
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]|)

proof end;

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 )

proof end;

theorem Th3: :: JGRAPH_7:3

for p1, p2 being Point of (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (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))

proof end;

theorem Th29: :: JGRAPH_7:29

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (TOP-REAL 2)
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 (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 " )

proof end;

theorem Th50: :: JGRAPH_7:50

for A, B, C, D being Real
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 ) )

proof end;

theorem Th51: :: JGRAPH_7:51

for A, B, C, D being Real
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 ) )

proof end;

theorem Th52: :: JGRAPH_7:52

for a, b, c, d being Real
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)

proof end;

theorem Th53: :: JGRAPH_7:53

for a, b, c, d being Real
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 )

proof end;

theorem Th54: :: JGRAPH_7:54

for a, b, c, d being Real
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

proof end;

theorem Th55: :: JGRAPH_7:55

for a, b, c, d being Real
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

proof end;

theorem Th56: :: JGRAPH_7:56

for a, b, c, d being Real
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

proof end;

theorem Th57: :: JGRAPH_7:57

for a, b, c, d being Real
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

proof end;

theorem Th58: :: JGRAPH_7:58

for a, b, c, d being Real
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 )

proof end;

theorem Th59: :: JGRAPH_7:59

for a, b, c, d being Real
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 )

proof end;

theorem Th60: :: JGRAPH_7:60

for a, b, c, d being Real
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 )

proof end;

theorem Th61: :: JGRAPH_7:61

for a, b, c, d being Real
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 )

proof end;

theorem Th62: :: JGRAPH_7:62

for a, b, c, d being Real
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 )

proof end;

theorem Th63: :: JGRAPH_7:63

for a, b, c, d being Real
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 )

proof end;

theorem Th64: :: JGRAPH_7:64

for a, b, c, d being Real
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 )

proof end;

theorem Th65: :: JGRAPH_7:65

for a, b, c, d being Real
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 )

proof end;

theorem Th66: :: JGRAPH_7:66

for a, b, c, d being Real
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 )

proof end;

theorem Th67: :: JGRAPH_7:67

for a, b, c, d being Real
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 )

proof end;

theorem Th68: :: JGRAPH_7:68

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem :: JGRAPH_7:69

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem Th70: :: JGRAPH_7:70

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem :: JGRAPH_7:71

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem Th72: :: JGRAPH_7:72

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem :: JGRAPH_7:73

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem Th74: :: JGRAPH_7:74

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem :: JGRAPH_7:75

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem Th76: :: JGRAPH_7:76

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem :: JGRAPH_7:77

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem Th78: :: JGRAPH_7:78

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem :: JGRAPH_7:79

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem Th80: :: JGRAPH_7:80

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem :: JGRAPH_7:81

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem Th82: :: JGRAPH_7:82

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem :: JGRAPH_7:83

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem Th84: :: JGRAPH_7:84

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem :: JGRAPH_7:85

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem Th86: :: JGRAPH_7:86

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem :: JGRAPH_7:87

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem Th88: :: JGRAPH_7:88

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem :: JGRAPH_7:89

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem Th90: :: JGRAPH_7:90

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem :: JGRAPH_7:91

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem Th92: :: JGRAPH_7:92

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem :: JGRAPH_7:93

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem Th94: :: JGRAPH_7:94

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem :: JGRAPH_7:95

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem Th96: :: JGRAPH_7:96

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem :: JGRAPH_7:97

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem Th98: :: JGRAPH_7:98

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem :: JGRAPH_7:99

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem Th100: :: JGRAPH_7:100

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem :: JGRAPH_7:101

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem Th102: :: JGRAPH_7:102

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem :: JGRAPH_7:103

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem Th104: :: JGRAPH_7:104

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem :: JGRAPH_7:105

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem Th106: :: JGRAPH_7:106

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem :: JGRAPH_7:107

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem Th108: :: JGRAPH_7:108

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem :: JGRAPH_7:109

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem Th110: :: JGRAPH_7:110

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem :: JGRAPH_7:111

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem Th112: :: JGRAPH_7:112

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem :: JGRAPH_7:113

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem Th114: :: JGRAPH_7:114

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem :: JGRAPH_7:115

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem Th116: :: JGRAPH_7:116

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem :: JGRAPH_7:117

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem Th118: :: JGRAPH_7:118

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem :: JGRAPH_7:119

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem Th120: :: JGRAPH_7:120

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem :: JGRAPH_7:121

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem Th122: :: JGRAPH_7:122

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem :: JGRAPH_7:123

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem Th124: :: JGRAPH_7:124

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem :: JGRAPH_7:125

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem Th126: :: JGRAPH_7:126

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem :: JGRAPH_7:127

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem Th128: :: JGRAPH_7:128

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem :: JGRAPH_7:129

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem Th130: :: JGRAPH_7:130

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem :: JGRAPH_7:131

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem Th132: :: JGRAPH_7:132

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem :: JGRAPH_7:133

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem Th134: :: JGRAPH_7:134

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem :: JGRAPH_7:135

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem Th136: :: JGRAPH_7:136

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;

theorem :: JGRAPH_7:137

for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being Real
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

proof end;