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

theorem Th1: :: JORDAN1J:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Go-board
for i1, i2, j1, j2 being Nat st 1 <= j1 & j1 <= width G & 1 <= j2 & j2 <= width G & 1 <= i1 & i1 < i2 & i2 <= len G holds
(G * i1,j1) `1 < (G * i2,j2) `1
proof end;

theorem Th2: :: JORDAN1J:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Go-board
for i1, i2, j1, j2 being Nat st 1 <= i1 & i1 <= len G & 1 <= i2 & i2 <= len G & 1 <= j1 & j1 < j2 & j2 <= width G holds
(G * i1,j1) `2 < (G * i2,j2) `2
proof end;

registration
let f be non empty FinSequence;
let g be FinSequence;
cluster f ^' g -> non empty ;
coherence
not f ^' g is empty
proof end;
end;

theorem Th3: :: JORDAN1J:3  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) -: (E-max (L~ (Cage C,n))))) /\ (L~ ((Cage C,n) :- (E-max (L~ (Cage C,n))))) = {(N-min (L~ (Cage C,n))),(E-max (L~ (Cage C,n)))}
proof end;

theorem Th4: :: JORDAN1J: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 = (Rotate (Cage C,n),(E-max (L~ (Cage C,n)))) :- (W-min (L~ (Cage C,n)))
proof end;

theorem :: JORDAN1J: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 compact non horizontal non vertical Subset of (TOP-REAL 2) holds
( W-min (L~ (Cage C,n)) in rng (Upper_Seq C,n) & W-min (L~ (Cage C,n)) in L~ (Upper_Seq C,n) )
proof end;

theorem :: JORDAN1J:6  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-max (L~ (Cage C,n)) in rng (Upper_Seq C,n) & W-max (L~ (Cage C,n)) in L~ (Upper_Seq C,n) )
proof end;

theorem Th7: :: JORDAN1J:7  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
( N-min (L~ (Cage C,n)) in rng (Upper_Seq C,n) & N-min (L~ (Cage C,n)) in L~ (Upper_Seq C,n) )
proof end;

theorem :: JORDAN1J:8  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
( N-max (L~ (Cage C,n)) in rng (Upper_Seq C,n) & N-max (L~ (Cage C,n)) in L~ (Upper_Seq C,n) )
proof end;

theorem :: JORDAN1J:9  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)) in rng (Upper_Seq C,n) & E-max (L~ (Cage C,n)) in L~ (Upper_Seq C,n) )
proof end;

theorem :: JORDAN1J:10  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)) in rng (Lower_Seq C,n) & E-max (L~ (Cage C,n)) in L~ (Lower_Seq C,n) )
proof end;

theorem :: JORDAN1J:11  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-min (L~ (Cage C,n)) in rng (Lower_Seq C,n) & E-min (L~ (Cage C,n)) in L~ (Lower_Seq C,n) )
proof end;

theorem Th12: :: JORDAN1J:12  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
( S-max (L~ (Cage C,n)) in rng (Lower_Seq C,n) & S-max (L~ (Cage C,n)) in L~ (Lower_Seq C,n) )
proof end;

theorem :: JORDAN1J:13  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
( S-min (L~ (Cage C,n)) in rng (Lower_Seq C,n) & S-min (L~ (Cage C,n)) in L~ (Lower_Seq C,n) )
proof end;

theorem :: JORDAN1J:14  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)) in rng (Lower_Seq C,n) & W-min (L~ (Cage C,n)) in L~ (Lower_Seq C,n) )
proof end;

theorem :: JORDAN1J:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & N-min Y in X holds
N-min X = N-min Y
proof end;

theorem :: JORDAN1J:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & N-max Y in X holds
N-max X = N-max Y
proof end;

theorem :: JORDAN1J:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & E-min Y in X holds
E-min X = E-min Y
proof end;

theorem :: JORDAN1J:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & E-max Y in X holds
E-max X = E-max Y
proof end;

theorem :: JORDAN1J:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & S-min Y in X holds
S-min X = S-min Y
proof end;

theorem :: JORDAN1J:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & S-max Y in X holds
S-max X = S-max Y
proof end;

theorem Th21: :: JORDAN1J:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & W-min Y in X holds
W-min X = W-min Y
proof end;

theorem :: JORDAN1J:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty compact Subset of (TOP-REAL 2) st X c= Y & W-max Y in X holds
W-max X = W-max Y
proof end;

theorem Th23: :: JORDAN1J:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty compact Subset of (TOP-REAL 2) st N-bound X <= N-bound Y holds
N-bound (X \/ Y) = N-bound Y
proof end;

theorem Th24: :: JORDAN1J:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty compact Subset of (TOP-REAL 2) st E-bound X <= E-bound Y holds
E-bound (X \/ Y) = E-bound Y
proof end;

theorem Th25: :: JORDAN1J:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty compact Subset of (TOP-REAL 2) st S-bound X <= S-bound Y holds
S-bound (X \/ Y) = S-bound X
proof end;

theorem Th26: :: JORDAN1J:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty compact Subset of (TOP-REAL 2) st W-bound X <= W-bound Y holds
W-bound (X \/ Y) = W-bound X
proof end;

theorem :: JORDAN1J:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty compact Subset of (TOP-REAL 2) st N-bound X < N-bound Y holds
N-min (X \/ Y) = N-min Y
proof end;

theorem :: JORDAN1J:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty compact Subset of (TOP-REAL 2) st N-bound X < N-bound Y holds
N-max (X \/ Y) = N-max Y
proof end;

theorem :: JORDAN1J:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty compact Subset of (TOP-REAL 2) st E-bound X < E-bound Y holds
E-min (X \/ Y) = E-min Y
proof end;

theorem :: JORDAN1J:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty compact Subset of (TOP-REAL 2) st E-bound X < E-bound Y holds
E-max (X \/ Y) = E-max Y
proof end;

theorem :: JORDAN1J:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty compact Subset of (TOP-REAL 2) st S-bound X < S-bound Y holds
S-min (X \/ Y) = S-min X
proof end;

theorem :: JORDAN1J:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty compact Subset of (TOP-REAL 2) st S-bound X < S-bound Y holds
S-max (X \/ Y) = S-max X
proof end;

theorem Th33: :: JORDAN1J:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty compact Subset of (TOP-REAL 2) st W-bound X < W-bound Y holds
W-min (X \/ Y) = W-min X
proof end;

theorem :: JORDAN1J:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being non empty compact Subset of (TOP-REAL 2) st W-bound X < W-bound Y holds
W-max (X \/ Y) = W-max X
proof end;

theorem Th35: :: JORDAN1J:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st f is_S-Seq & p in L~ f holds
(L_Cut f,p) /. (len (L_Cut f,p)) = f /. (len f)
proof end;

theorem Th36: :: JORDAN1J:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being non constant standard special_circular_sequence
for p, q being Point of (TOP-REAL 2)
for g being connected Subset of (TOP-REAL 2) st p in RightComp f & q in LeftComp f & p in g & q in g holds
g meets L~ f
proof end;

registration
cluster non constant being_S-Seq s.c.c. standard FinSequence of the carrier of (TOP-REAL 2);
existence
ex b1 being being_S-Seq FinSequence of (TOP-REAL 2) st
( not b1 is constant & b1 is standard & b1 is s.c.c. )
proof end;
end;

theorem Th37: :: JORDAN1J:37  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
L_Cut f,p = mid f,(p .. f),(len f)
proof end;

theorem Th38: :: JORDAN1J:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being Go-board
for f being S-Sequence_in_R2 st f is_sequence_on M holds
for p being Point of (TOP-REAL 2) st p in rng f holds
R_Cut f,p is_sequence_on M
proof end;

theorem Th39: :: JORDAN1J:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for M being Go-board
for f being S-Sequence_in_R2 st f is_sequence_on M holds
for p being Point of (TOP-REAL 2) st p in rng f holds
L_Cut f,p is_sequence_on M
proof end;

theorem Th40: :: JORDAN1J:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Go-board
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G holds
for i, j being Nat st 1 <= i & i <= len G & 1 <= j & j <= width G & G * i,j in L~ f holds
G * i,j in rng f
proof end;

theorem :: JORDAN1J:41  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 g being FinSequence of (TOP-REAL 2) st g is unfolded & g is s.n.c. & g is one-to-one & (L~ f) /\ (L~ g) = {(f /. 1)} & f /. 1 = g /. (len g) & ( for i being Nat st 1 <= i & i + 2 <= len f holds
(LSeg f,i) /\ (LSeg (f /. (len f)),(g /. 1)) = {} ) & ( for i being Nat st 2 <= i & i + 1 <= len g holds
(LSeg g,i) /\ (LSeg (f /. (len f)),(g /. 1)) = {} ) holds
f ^ g is s.c.c.
proof end;

theorem :: JORDAN1J: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 non empty compact non horizontal non vertical Subset of (TOP-REAL 2) ex i being Nat st
( 1 <= i & i + 1 <= len (Gauge C,n) & W-min C in cell (Gauge C,n),1,i & W-min C <> (Gauge C,n) * 2,i )
proof end;

theorem Th43: :: JORDAN1J:43  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 L~ f & f . (len f) in L~ (R_Cut f,p) holds
f . (len f) = p
proof end;

theorem Th44: :: JORDAN1J:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) holds R_Cut f,p <> {}
proof end;

theorem Th45: :: JORDAN1J:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in L~ f holds
(R_Cut f,p) /. (len (R_Cut f,p)) = p
proof end;

theorem Th46: :: JORDAN1J:46  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 p being Point of (TOP-REAL 2) st p in L~ (Upper_Seq C,n) & p `1 = E-bound (L~ (Cage C,n)) holds
p = E-max (L~ (Cage C,n))
proof end;

theorem :: JORDAN1J:47  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 p being Point of (TOP-REAL 2) st p in L~ (Lower_Seq C,n) & p `1 = W-bound (L~ (Cage C,n)) holds
p = W-min (L~ (Cage C,n))
proof end;

theorem :: JORDAN1J:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Go-board
for f, g being FinSequence of (TOP-REAL 2)
for k being Nat st 1 <= k & k < len f & f ^ g is_sequence_on G holds
( left_cell (f ^ g),k,G = left_cell f,k,G & right_cell (f ^ g),k,G = right_cell f,k,G )
proof end;

theorem Th49: :: JORDAN1J:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being set
for f, g being FinSequence of D
for i being Nat st i <= len f holds
(f ^' g) | i = f | i
proof end;

theorem Th50: :: JORDAN1J:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being set
for f, g being FinSequence of D holds (f ^' g) | (len f) = f
proof end;

theorem Th51: :: JORDAN1J:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Go-board
for f, g being FinSequence of (TOP-REAL 2)
for k being Nat st 1 <= k & k < len f & f ^' g is_sequence_on G holds
( left_cell (f ^' g),k,G = left_cell f,k,G & right_cell (f ^' g),k,G = right_cell f,k,G )
proof end;

theorem Th52: :: JORDAN1J:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Go-board
for f being S-Sequence_in_R2
for p being Point of (TOP-REAL 2)
for k being Nat st 1 <= k & k < p .. f & f is_sequence_on G & p in rng f holds
( left_cell (R_Cut f,p),k,G = left_cell f,k,G & right_cell (R_Cut f,p),k,G = right_cell f,k,G )
proof end;

theorem Th53: :: JORDAN1J:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Go-board
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2)
for k being Nat st 1 <= k & k < p .. f & f is_sequence_on G holds
( left_cell (f -: p),k,G = left_cell f,k,G & right_cell (f -: p),k,G = right_cell f,k,G )
proof end;

theorem Th54: :: JORDAN1J:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being FinSequence of (TOP-REAL 2) st f is unfolded & f is s.n.c. & f is one-to-one & g is unfolded & g is s.n.c. & g is one-to-one & f /. (len f) = g /. 1 & (L~ f) /\ (L~ g) = {(g /. 1)} holds
f ^' g is s.n.c.
proof end;

theorem Th55: :: JORDAN1J:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g being FinSequence of (TOP-REAL 2) st f is one-to-one & g is one-to-one & (rng f) /\ (rng g) c= {(g /. 1)} holds
f ^' g is one-to-one
proof end;

theorem Th56: :: JORDAN1J:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st f is_S-Seq & p in rng f & p <> f . 1 holds
(Index p,f) + 1 = p .. f
proof end;

theorem Th57: :: JORDAN1J:57  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, k being Nat st 1 < i & i < len (Gauge C,n) & 1 <= j & k <= width (Gauge C,n) & (Gauge C,n) * i,k in L~ (Upper_Seq C,n) & (Gauge C,n) * i,j in L~ (Lower_Seq C,n) holds
j <> k
proof end;

theorem Th58: :: JORDAN1J:58  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 Simple_closed_curve
for i, j, k being Nat st 1 < i & i < len (Gauge C,n) & 1 <= j & j <= k & k <= width (Gauge C,n) & (LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * i,k)} & (LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * i,j)} holds
LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k) meets Lower_Arc C
proof end;

theorem Th59: :: JORDAN1J:59  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 Simple_closed_curve
for i, j, k being Nat st 1 < i & i < len (Gauge C,n) & 1 <= j & j <= k & k <= width (Gauge C,n) & (LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Upper_Seq C,n)) = {((Gauge C,n) * i,k)} & (LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (L~ (Lower_Seq C,n)) = {((Gauge C,n) * i,j)} holds
LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k) meets Upper_Arc C
proof end;

theorem Th60: :: JORDAN1J:60  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 Simple_closed_curve
for i, j, k being Nat st 1 < i & i < len (Gauge C,n) & 1 <= j & j <= k & k <= width (Gauge C,n) & n > 0 & (LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (Upper_Arc (L~ (Cage C,n))) = {((Gauge C,n) * i,k)} & (LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (Lower_Arc (L~ (Cage C,n))) = {((Gauge C,n) * i,j)} holds
LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k) meets Lower_Arc C
proof end;

theorem Th61: :: JORDAN1J:61  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 Simple_closed_curve
for i, j, k being Nat st 1 < i & i < len (Gauge C,n) & 1 <= j & j <= k & k <= width (Gauge C,n) & n > 0 & (LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (Upper_Arc (L~ (Cage C,n))) = {((Gauge C,n) * i,k)} & (LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k)) /\ (Lower_Arc (L~ (Cage C,n))) = {((Gauge C,n) * i,j)} holds
LSeg ((Gauge C,n) * i,j),((Gauge C,n) * i,k) meets Upper_Arc C
proof end;

theorem :: JORDAN1J:62  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 j being Nat st (Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j in Upper_Arc (L~ (Cage C,(n + 1))) & 1 <= j & j <= width (Gauge C,(n + 1)) holds
LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j) meets Lower_Arc (L~ (Cage C,(n + 1)))
proof end;

theorem :: JORDAN1J:63  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 Simple_closed_curve
for j, k being Nat st 1 <= j & j <= k & k <= width (Gauge C,(n + 1)) & (LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k)) /\ (Upper_Arc (L~ (Cage C,(n + 1)))) = {((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k)} & (LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k)) /\ (Lower_Arc (L~ (Cage C,(n + 1)))) = {((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j)} holds
LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k) meets Lower_Arc C
proof end;

theorem :: JORDAN1J:64  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 Simple_closed_curve
for j, k being Nat st 1 <= j & j <= k & k <= width (Gauge C,(n + 1)) & (LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k)) /\ (Upper_Arc (L~ (Cage C,(n + 1)))) = {((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k)} & (LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k)) /\ (Lower_Arc (L~ (Cage C,(n + 1)))) = {((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j)} holds
LSeg ((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),j),((Gauge C,(n + 1)) * (Center (Gauge C,(n + 1))),k) meets Upper_Arc C
proof end;