:: JGRAPH_7 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: JGRAPH_7:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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]|
proof end;

theorem Th2: :: JGRAPH_7:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th4: :: JGRAPH_7:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th5: :: JGRAPH_7:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th6: :: JGRAPH_7:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th7: :: JGRAPH_7:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th8: :: JGRAPH_7:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th9: :: JGRAPH_7:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th10: :: JGRAPH_7:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th11: :: JGRAPH_7:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th12: :: JGRAPH_7:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th13: :: JGRAPH_7:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th14: :: JGRAPH_7:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2, p3, p4 being Point of (TOP-REAL 2)
for a, b, c, d being real number st a < b & c < d & p1 `1 = a & p2 `1 = a & p3 `1 = a & p4 `1 = a & c <= p1 `2 & p1 `2 < p2 `2 & p2 `2 < p3 `2 & p3 `2 < p4 `2 & p4 `2 <= d holds
p1,p2,p3,p4 are_in_this_order_on rectangle a,b,c,d
proof end;

theorem Th15: :: JGRAPH_7:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th16: :: JGRAPH_7:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th17: :: JGRAPH_7:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th18: :: JGRAPH_7:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th19: :: JGRAPH_7:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th20: :: JGRAPH_7:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th21: :: JGRAPH_7:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th22: :: JGRAPH_7:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th23: :: JGRAPH_7:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th24: :: JGRAPH_7:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th25: :: JGRAPH_7:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th26: :: JGRAPH_7:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th27: :: JGRAPH_7:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th28: :: JGRAPH_7:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th30: :: JGRAPH_7:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th31: :: JGRAPH_7:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th32: :: JGRAPH_7:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th33: :: JGRAPH_7:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th34: :: JGRAPH_7:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th35: :: JGRAPH_7:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th36: :: JGRAPH_7:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th37: :: JGRAPH_7:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th38: :: JGRAPH_7:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th39: :: JGRAPH_7:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th40: :: JGRAPH_7:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th41: :: JGRAPH_7:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th42: :: JGRAPH_7:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th43: :: JGRAPH_7:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th44: :: JGRAPH_7:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th45: :: JGRAPH_7:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th46: :: JGRAPH_7:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th47: :: JGRAPH_7:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th48: :: JGRAPH_7:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th49: :: JGRAPH_7:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 " )
proof end;

theorem Th50: :: JGRAPH_7:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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_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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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_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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th53: :: JGRAPH_7:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th54: :: JGRAPH_7:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & c < d & 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & c < d & 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 < (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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th60: :: JGRAPH_7:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th62: :: JGRAPH_7:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 < (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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th64: :: JGRAPH_7:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 & 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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))) & 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th67: :: JGRAPH_7:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 . 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;

set K = rectangle (- 1),1,(- 1),1;

theorem Th68: :: JGRAPH_7:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: JGRAPH_7:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th70: :: JGRAPH_7:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: JGRAPH_7:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th72: :: JGRAPH_7:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: JGRAPH_7:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th74: :: JGRAPH_7:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: JGRAPH_7:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th76: :: JGRAPH_7:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: JGRAPH_7:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th78: :: JGRAPH_7:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: JGRAPH_7:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th80: :: JGRAPH_7:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: JGRAPH_7:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th82: :: JGRAPH_7:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: JGRAPH_7:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th84: :: JGRAPH_7:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: JGRAPH_7:85  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th86: :: JGRAPH_7:86  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: JGRAPH_7:87  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th88: :: JGRAPH_7:88  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: JGRAPH_7:89  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th90: :: JGRAPH_7:90  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: JGRAPH_7:91  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th92: :: JGRAPH_7:92  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: JGRAPH_7:93  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th94: :: JGRAPH_7:94  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: JGRAPH_7:95  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th96: :: JGRAPH_7:96  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: JGRAPH_7:97  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th98: :: JGRAPH_7:98  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: JGRAPH_7:99  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th100: :: JGRAPH_7:100  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: JGRAPH_7:101  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th102: :: JGRAPH_7:102  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: JGRAPH_7:103  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th104: :: JGRAPH_7:104  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: JGRAPH_7:105  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th106: :: JGRAPH_7:106  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: JGRAPH_7:107  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th108: :: JGRAPH_7:108  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: JGRAPH_7:109  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th110: :: JGRAPH_7:110  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: JGRAPH_7:111  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th112: :: JGRAPH_7:112  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: JGRAPH_7:113  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th114: :: JGRAPH_7:114  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: JGRAPH_7:115  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th116: :: JGRAPH_7:116  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: JGRAPH_7:117  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th118: :: JGRAPH_7:118  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: JGRAPH_7:119  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th120: :: JGRAPH_7:120  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: JGRAPH_7:121  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th122: :: JGRAPH_7:122  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: JGRAPH_7:123  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th124: :: JGRAPH_7:124  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: JGRAPH_7:125  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th126: :: JGRAPH_7:126  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: JGRAPH_7:127  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th128: :: JGRAPH_7:128  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: JGRAPH_7:129  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th130: :: JGRAPH_7:130  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: JGRAPH_7:131  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th132: :: JGRAPH_7:132  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: JGRAPH_7:133  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th134: :: JGRAPH_7:134  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: JGRAPH_7:135  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th136: :: JGRAPH_7:136  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: JGRAPH_7:137  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;