:: JGRAPH_8 semantic presentation

Lemma1: I[01] = TopSpaceMetr (Closed-Interval-MSpace 0,1)
by TOPMETR:27, TOPMETR:def 8;

Lemma2: for b1 being set
for b2 being FinSequence st 1 <= len b2 holds
( (b2 ^ <*b1*>) . 1 = b2 . 1 & (<*b1*> ^ b2) . ((len b2) + 1) = b2 . (len b2) )
proof end;

Lemma3: for b1 being FinSequence of REAL st ( for b2 being Nat st 1 <= b2 & b2 < len b1 holds
b1 /. b2 < b1 /. (b2 + 1) ) holds
b1 is increasing
proof end;

registration
let c1, c2, c3, c4 be real number ;
cluster closed_inside_of_rectangle a1,a2,a3,a4 -> convex ;
coherence
closed_inside_of_rectangle c1,c2,c3,c4 is convex
proof end;
end;

registration
let c1, c2, c3, c4 be real number ;
cluster Trectangle a1,a2,a3,a4 -> convex ;
coherence
Trectangle c1,c2,c3,c4 is convex
proof end;
end;

theorem Th1: :: JGRAPH_8:1
for b1 being Nat
for b2 being real positive number
for b3 being continuous Function of I[01] ,(TOP-REAL b1) ex b4 being FinSequence of REAL st
( b4 . 1 = 0 & b4 . (len b4) = 1 & 5 <= len b4 & rng b4 c= the carrier of I[01] & b4 is increasing & ( for b5 being Nat
for b6 being Subset of I[01]
for b7 being Subset of (Euclid b1) st 1 <= b5 & b5 < len b4 & b6 = [.(b4 /. b5),(b4 /. (b5 + 1)).] & b7 = b3 .: b6 holds
diameter b7 < b2 ) )
proof end;

theorem Th2: :: JGRAPH_8:2
for b1 being Nat
for b2, b3 being Point of (TOP-REAL b1)
for b4 being Subset of (TOP-REAL b1) st b4 c= LSeg b2,b3 & b2 in b4 & b3 in b4 & b4 is connected holds
b4 = LSeg b2,b3
proof end;

theorem Th3: :: JGRAPH_8:3
for b1 being Nat
for b2, b3 being Point of (TOP-REAL b1)
for b4 being Path of b2,b3 st rng b4 c= LSeg b2,b3 holds
rng b4 = LSeg b2,b3
proof end;

theorem Th4: :: JGRAPH_8:4
for b1, b2 being non empty Subset of (TOP-REAL 2)
for b3, b4, b5, b6 being Point of (TOP-REAL 2)
for b7 being Path of b3,b4
for b8 being Path of b5,b6 st rng b7 = b1 & rng b8 = b2 & ( for b9 being Point of (TOP-REAL 2) st b9 in b1 holds
( b3 `1 <= b9 `1 & b9 `1 <= b4 `1 ) ) & ( for b9 being Point of (TOP-REAL 2) st b9 in b2 holds
( b3 `1 <= b9 `1 & b9 `1 <= b4 `1 ) ) & ( for b9 being Point of (TOP-REAL 2) st b9 in b1 holds
( b5 `2 <= b9 `2 & b9 `2 <= b6 `2 ) ) & ( for b9 being Point of (TOP-REAL 2) st b9 in b2 holds
( b5 `2 <= b9 `2 & b9 `2 <= b6 `2 ) ) holds
b1 meets b2
proof end;

theorem Th5: :: JGRAPH_8:5
for b1, b2, b3, b4 being real number
for b5, b6 being continuous Function of I[01] ,(TOP-REAL 2)
for b7, b8 being Point of I[01] st b7 = 0 & b8 = 1 & (b5 . b7) `1 = b1 & (b5 . b8) `1 = b2 & (b6 . b7) `2 = b3 & (b6 . b8) `2 = b4 & ( for b9 being Point of I[01] holds
( b1 <= (b5 . b9) `1 & (b5 . b9) `1 <= b2 & b1 <= (b6 . b9) `1 & (b6 . b9) `1 <= b2 & b3 <= (b5 . b9) `2 & (b5 . b9) `2 <= b4 & b3 <= (b6 . b9) `2 & (b6 . b9) `2 <= b4 ) ) holds
rng b5 meets rng b6
proof end;

theorem Th6: :: JGRAPH_8:6
for b1, b2, b3, b4 being real number
for b5, b6, b7, b8 being Point of (Trectangle b1,b2,b3,b4)
for b9 being Path of b5,b6
for b10 being Path of b8,b7
for b11, b12, b13, b14 being Point of (TOP-REAL 2) st b11 `1 = b1 & b12 `1 = b2 & b13 `2 = b3 & b14 `2 = b4 & b5 = b11 & b6 = b12 & b7 = b13 & b8 = b14 holds
ex b15, b16 being Point of I[01] st b9 . b15 = b10 . b16
proof end;