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

registration
cluster trivial set ;
existence
ex b1 being FinSequence st b1 is trivial
proof end;
end;

theorem Th1: :: JORDAN1G:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being trivial FinSequence holds
( f is empty or ex x being set st f = <*x*> )
proof end;

registration
let p be non trivial FinSequence;
cluster Rev p -> non trivial ;
coherence
not Rev p is trivial
proof end;
end;

theorem Th2: :: JORDAN1G:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for f being FinSequence of D
for G being Matrix of D
for p being set st f is_sequence_on G holds
f -: p is_sequence_on G
proof end;

theorem Th3: :: JORDAN1G:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for f being FinSequence of D
for G being Matrix of D
for p being Element of D st p in rng f & f is_sequence_on G holds
f :- p is_sequence_on G
proof end;

theorem Th4: :: JORDAN1G:4  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 C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds Upper_Seq C,n is_sequence_on Gauge C,n
proof end;

theorem Th5: :: JORDAN1G:5  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 C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds Lower_Seq C,n is_sequence_on Gauge C,n
proof end;

registration
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2);
let n be Nat;
cluster Upper_Seq C,n -> standard ;
coherence
Upper_Seq C,n is standard
proof end;
cluster Lower_Seq C,n -> standard ;
coherence
Lower_Seq C,n is standard
proof end;
end;

theorem Th6: :: JORDAN1G:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Y_equal-in-column Y_increasing-in-line Matrix of (TOP-REAL 2)
for i1, i2, j1, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & (G * i1,j1) `2 = (G * i2,j2) `2 holds
j1 = j2
proof end;

theorem Th7: :: JORDAN1G:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being X_equal-in-line X_increasing-in-column Matrix of (TOP-REAL 2)
for i1, i2, j1, j2 being Nat st [i1,j1] in Indices G & [i2,j2] in Indices G & (G * i1,j1) `1 = (G * i2,j2) `1 holds
i1 = i2
proof end;

theorem :: JORDAN1G:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: JORDAN1G:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: JORDAN1G:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: JORDAN1G:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: JORDAN1G:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: JORDAN1G:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: JORDAN1G:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: JORDAN1G:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th16: :: JORDAN1G:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non trivial special unfolded standard FinSequence of (TOP-REAL 2) st ( ( f /. 1 <> N-min (L~ f) & f /. (len f) <> N-min (L~ f) ) or ( f /. 1 <> N-max (L~ f) & f /. (len f) <> N-max (L~ f) ) ) holds
(N-min (L~ f)) `1 < (N-max (L~ f)) `1
proof end;

theorem :: JORDAN1G:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non trivial special unfolded standard FinSequence of (TOP-REAL 2) st ( ( f /. 1 <> N-min (L~ f) & f /. (len f) <> N-min (L~ f) ) or ( f /. 1 <> N-max (L~ f) & f /. (len f) <> N-max (L~ f) ) ) holds
N-min (L~ f) <> N-max (L~ f)
proof end;

theorem Th18: :: JORDAN1G:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non trivial special unfolded standard FinSequence of (TOP-REAL 2) st ( ( f /. 1 <> S-min (L~ f) & f /. (len f) <> S-min (L~ f) ) or ( f /. 1 <> S-max (L~ f) & f /. (len f) <> S-max (L~ f) ) ) holds
(S-min (L~ f)) `1 < (S-max (L~ f)) `1
proof end;

theorem :: JORDAN1G:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non trivial special unfolded standard FinSequence of (TOP-REAL 2) st ( ( f /. 1 <> S-min (L~ f) & f /. (len f) <> S-min (L~ f) ) or ( f /. 1 <> S-max (L~ f) & f /. (len f) <> S-max (L~ f) ) ) holds
S-min (L~ f) <> S-max (L~ f)
proof end;

theorem Th20: :: JORDAN1G:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non trivial special unfolded standard FinSequence of (TOP-REAL 2) st ( ( f /. 1 <> W-min (L~ f) & f /. (len f) <> W-min (L~ f) ) or ( f /. 1 <> W-max (L~ f) & f /. (len f) <> W-max (L~ f) ) ) holds
(W-min (L~ f)) `2 < (W-max (L~ f)) `2
proof end;

theorem :: JORDAN1G:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non trivial special unfolded standard FinSequence of (TOP-REAL 2) st ( ( f /. 1 <> W-min (L~ f) & f /. (len f) <> W-min (L~ f) ) or ( f /. 1 <> W-max (L~ f) & f /. (len f) <> W-max (L~ f) ) ) holds
W-min (L~ f) <> W-max (L~ f)
proof end;

theorem Th22: :: JORDAN1G:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non trivial special unfolded standard FinSequence of (TOP-REAL 2) st ( ( f /. 1 <> E-min (L~ f) & f /. (len f) <> E-min (L~ f) ) or ( f /. 1 <> E-max (L~ f) & f /. (len f) <> E-max (L~ f) ) ) holds
(E-min (L~ f)) `2 < (E-max (L~ f)) `2
proof end;

theorem :: JORDAN1G:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non trivial special unfolded standard FinSequence of (TOP-REAL 2) st ( ( f /. 1 <> E-min (L~ f) & f /. (len f) <> E-min (L~ f) ) or ( f /. 1 <> E-max (L~ f) & f /. (len f) <> E-max (L~ f) ) ) holds
E-min (L~ f) <> E-max (L~ f)
proof end;

theorem Th24: :: JORDAN1G:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being non empty set
for f being FinSequence of D
for p, q being Element of D st p in rng f & q in rng f & q .. f <= p .. f holds
(f -: p) :- q = (f :- q) -: p
proof end;

theorem Th25: :: JORDAN1G:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds (L~ ((Cage C,n) -: (W-min (L~ (Cage C,n))))) /\ (L~ ((Cage C,n) :- (W-min (L~ (Cage C,n))))) = {(N-min (L~ (Cage C,n))),(W-min (L~ (Cage C,n)))}
proof end;

theorem Th26: :: JORDAN1G:26  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 C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds Lower_Seq C,n = (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) -: (W-min (L~ (Cage C,n)))
proof end;

theorem Th27: :: JORDAN1G:27  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 C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds (W-min (L~ (Cage C,n))) .. (Upper_Seq C,n) = 1
proof end;

theorem Th28: :: JORDAN1G:28  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 C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds (W-min (L~ (Cage C,n))) .. (Upper_Seq C,n) < (W-max (L~ (Cage C,n))) .. (Upper_Seq C,n)
proof end;

theorem Th29: :: JORDAN1G:29  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 C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds (W-max (L~ (Cage C,n))) .. (Upper_Seq C,n) <= (N-min (L~ (Cage C,n))) .. (Upper_Seq C,n)
proof end;

theorem Th30: :: JORDAN1G:30  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 C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds (N-min (L~ (Cage C,n))) .. (Upper_Seq C,n) < (N-max (L~ (Cage C,n))) .. (Upper_Seq C,n)
proof end;

theorem Th31: :: JORDAN1G:31  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 C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds (N-max (L~ (Cage C,n))) .. (Upper_Seq C,n) <= (E-max (L~ (Cage C,n))) .. (Upper_Seq C,n)
proof end;

theorem Th32: :: JORDAN1G:32  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 C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds (E-max (L~ (Cage C,n))) .. (Upper_Seq C,n) = len (Upper_Seq C,n)
proof end;

theorem Th33: :: JORDAN1G:33  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 C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds (E-max (L~ (Cage C,n))) .. (Lower_Seq C,n) = 1
proof end;

theorem Th34: :: JORDAN1G:34  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 C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (E-max (L~ (Cage C,n))) .. (Lower_Seq C,n) < (E-min (L~ (Cage C,n))) .. (Lower_Seq C,n)
proof end;

theorem Th35: :: JORDAN1G:35  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 C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (E-min (L~ (Cage C,n))) .. (Lower_Seq C,n) <= (S-max (L~ (Cage C,n))) .. (Lower_Seq C,n)
proof end;

theorem Th36: :: JORDAN1G:36  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 C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (S-max (L~ (Cage C,n))) .. (Lower_Seq C,n) < (S-min (L~ (Cage C,n))) .. (Lower_Seq C,n)
proof end;

theorem Th37: :: JORDAN1G:37  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 C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (S-min (L~ (Cage C,n))) .. (Lower_Seq C,n) <= (W-min (L~ (Cage C,n))) .. (Lower_Seq C,n)
proof end;

theorem Th38: :: JORDAN1G:38  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 C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (W-min (L~ (Cage C,n))) .. (Lower_Seq C,n) = len (Lower_Seq C,n)
proof end;

theorem Th39: :: JORDAN1G:39  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 C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds ((Upper_Seq C,n) /. 2) `1 = W-bound (L~ (Cage C,n))
proof end;

theorem :: JORDAN1G:40  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 C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds ((Lower_Seq C,n) /. 2) `1 = E-bound (L~ (Cage C,n))
proof end;

theorem Th41: :: JORDAN1G:41  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 C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n))) = (W-bound C) + (E-bound C)
proof end;

theorem :: JORDAN1G:42  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 C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds (S-bound (L~ (Cage C,n))) + (N-bound (L~ (Cage C,n))) = (S-bound C) + (N-bound C)
proof end;

theorem Th43: :: JORDAN1G:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for n, i being Nat st 1 <= i & i <= width (Gauge C,n) & n > 0 holds
((Gauge C,n) * (Center (Gauge C,n)),i) `1 = ((W-bound C) + (E-bound C)) / 2
proof end;

theorem :: JORDAN1G:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for n, i being Nat st 1 <= i & i <= len (Gauge C,n) & n > 0 holds
((Gauge C,n) * i,(Center (Gauge C,n))) `2 = ((S-bound C) + (N-bound C)) / 2
proof end;

theorem Th45: :: JORDAN1G:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being S-Sequence_in_R2
for k1, k2 being Nat st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f & f /. 1 in L~ (mid f,k1,k2) & not k1 = 1 holds
k2 = 1
proof end;

theorem Th46: :: JORDAN1G:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being S-Sequence_in_R2
for k1, k2 being Nat st 1 <= k1 & k1 <= len f & 1 <= k2 & k2 <= len f & f /. (len f) in L~ (mid f,k1,k2) & not k1 = len f holds
k2 = len f
proof end;

theorem Th47: :: JORDAN1G:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds
( rng (Upper_Seq C,n) c= rng (Cage C,n) & rng (Lower_Seq C,n) c= rng (Cage C,n) )
proof end;

theorem Th48: :: JORDAN1G:48  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 C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds Upper_Seq C,n is_a_h.c._for Cage C,n
proof end;

theorem Th49: :: JORDAN1G:49  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 C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds Rev (Lower_Seq C,n) is_a_h.c._for Cage C,n
proof end;

theorem Th50: :: JORDAN1G:50  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 C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i being Nat st 1 < i & i <= len (Gauge C,n) holds
not (Gauge C,n) * i,1 in rng (Upper_Seq C,n)
proof end;

theorem Th51: :: JORDAN1G:51  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 C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i being Nat st 1 <= i & i < len (Gauge C,n) holds
not (Gauge C,n) * i,(width (Gauge C,n)) in rng (Lower_Seq C,n)
proof end;

theorem Th52: :: JORDAN1G:52  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 C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i being Nat st 1 < i & i <= len (Gauge C,n) holds
not (Gauge C,n) * i,1 in L~ (Upper_Seq C,n)
proof end;

theorem :: JORDAN1G:53  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 C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i being Nat st 1 <= i & i < len (Gauge C,n) holds
not (Gauge C,n) * i,(width (Gauge C,n)) in L~ (Lower_Seq C,n)
proof end;

theorem Th54: :: JORDAN1G:54  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 C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j being Nat st 1 <= i & i <= len (Gauge C,n) & 1 <= j & j <= width (Gauge C,n) & (Gauge C,n) * i,j in L~ (Cage C,n) holds
LSeg ((Gauge C,n) * i,1),((Gauge C,n) * i,j) meets L~ (Lower_Seq C,n)
proof end;

theorem Th55: :: JORDAN1G:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat st n > 0 holds
First_Point (L~ (Upper_Seq C,n)),(W-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n))),(Vertical_Line (((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2)) in rng (Upper_Seq C,n)
proof end;

theorem Th56: :: JORDAN1G:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat st n > 0 holds
Last_Point (L~ (Lower_Seq C,n)),(E-max (L~ (Cage C,n))),(W-min (L~ (Cage C,n))),(Vertical_Line (((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2)) in rng (Lower_Seq C,n)
proof end;

theorem Th57: :: JORDAN1G:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being S-Sequence_in_R2
for p being Point of (TOP-REAL 2) st p in rng f holds
R_Cut f,p = mid f,1,(p .. f)
proof end;

theorem Th58: :: JORDAN1G:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being S-Sequence_in_R2
for Q being closed Subset of (TOP-REAL 2) st L~ f meets Q & not f /. 1 in Q & First_Point (L~ f),(f /. 1),(f /. (len f)),Q in rng f holds
(L~ (mid f,1,((First_Point (L~ f),(f /. 1),(f /. (len f)),Q) .. f))) /\ Q = {(First_Point (L~ f),(f /. 1),(f /. (len f)),Q)}
proof end;

theorem Th59: :: JORDAN1G:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat st n > 0 holds
for k being Nat st 1 <= k & k < (First_Point (L~ (Upper_Seq C,n)),(W-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n))),(Vertical_Line (((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2))) .. (Upper_Seq C,n) holds
((Upper_Seq C,n) /. k) `1 < ((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2
proof end;

theorem Th60: :: JORDAN1G:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat st n > 0 holds
for k being Nat st 1 <= k & k < (First_Point (L~ (Rev (Lower_Seq C,n))),(W-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n))),(Vertical_Line (((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2))) .. (Rev (Lower_Seq C,n)) holds
((Rev (Lower_Seq C,n)) /. k) `1 < ((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2
proof end;

theorem Th61: :: JORDAN1G:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat st n > 0 holds
for q being Point of (TOP-REAL 2) st q in rng (mid (Upper_Seq C,n),2,((First_Point (L~ (Upper_Seq C,n)),(W-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n))),(Vertical_Line (((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2))) .. (Upper_Seq C,n))) holds
q `1 <= ((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2
proof end;

theorem Th62: :: JORDAN1G:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat st n > 0 holds
(First_Point (L~ (Upper_Seq C,n)),(W-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n))),(Vertical_Line (((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2))) `2 > (Last_Point (L~ (Lower_Seq C,n)),(E-max (L~ (Cage C,n))),(W-min (L~ (Cage C,n))),(Vertical_Line (((W-bound (L~ (Cage C,n))) + (E-bound (L~ (Cage C,n)))) / 2))) `2
proof end;

theorem Th63: :: JORDAN1G:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat st n > 0 holds
L~ (Upper_Seq C,n) = Upper_Arc (L~ (Cage C,n))
proof end;

theorem Th64: :: JORDAN1G:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat st n > 0 holds
L~ (Lower_Seq C,n) = Lower_Arc (L~ (Cage C,n))
proof end;

theorem :: JORDAN1G:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat st n > 0 holds
for i, j being Nat st 1 <= i & i <= len (Gauge C,n) & 1 <= j & j <= width (Gauge C,n) & (Gauge C,n) * i,j in L~ (Cage C,n) holds
LSeg ((Gauge C,n) * i,1),((Gauge C,n) * i,j) meets Lower_Arc (L~ (Cage C,n))
proof end;