:: by Andrzej Trybulec

::

:: Received October 7, 2001

:: Copyright (c) 2001-2019 Association of Mizar Users

registration

let D be non empty with_non-empty_element set ;

ex b_{1} being FinSequence of D * st

( not b_{1} is empty & b_{1} is non-empty )

end;
cluster Relation-like non-empty NAT -defined D * -valued non empty Function-like finite FinSequence-like FinSubsequence-like Function-yielding V88() FinSequence-yielding finite-support for FinSequence of D * ;

existence ex b

( not b

proof end;

registration
end;

theorem :: JORDAN1H:3

for S being Subset of (TOP-REAL 2)

for p, q being Point of (TOP-REAL 2) st p <> q & (LSeg (p,q)) \ {p,q} c= S holds

LSeg (p,q) c= Cl S

for p, q being Point of (TOP-REAL 2) st p <> q & (LSeg (p,q)) \ {p,q} c= S holds

LSeg (p,q) c= Cl S

proof end;

Lm1: RealOrd is_reflexive_in REAL

;

Lm2: RealOrd is_antisymmetric_in REAL

proof end;

Lm3: RealOrd is_transitive_in REAL

proof end;

Lm4: RealOrd is_connected_in REAL

proof end;

registration

coherence

( RealOrd is total & RealOrd is reflexive & RealOrd is antisymmetric & RealOrd is transitive & RealOrd is being_linear-order )

end;
( RealOrd is total & RealOrd is reflexive & RealOrd is antisymmetric & RealOrd is transitive & RealOrd is being_linear-order )

proof end;

theorem Th8: :: JORDAN1H:8

for f being FinSequence of REAL

for A being finite Subset of REAL st A = rng f holds

SgmX (RealOrd,A) = Incr f

for A being finite Subset of REAL st A = rng f holds

SgmX (RealOrd,A) = Incr f

proof end;

theorem Th9: :: JORDAN1H:9

for X being non empty set

for A being finite Subset of X

for R being being_linear-order Order of X holds len (SgmX (R,A)) = card A

for A being finite Subset of X

for R being being_linear-order Order of X holds len (SgmX (R,A)) = card A

proof end;

definition

let D be non empty set ;

let M be FinSequence of D * ;

:: original: Values

redefine func Values M -> Subset of D;

coherence

Values M is Subset of D

end;
let M be FinSequence of D * ;

:: original: Values

redefine func Values M -> Subset of D;

coherence

Values M is Subset of D

proof end;

registration

let D be non empty with_non-empty_elements set ;

let M be non-empty non empty FinSequence of D * ;

coherence

not Values M is empty

end;
let M be non-empty non empty FinSequence of D * ;

coherence

not Values M is empty

proof end;

theorem Th12: :: JORDAN1H:12

for D being non empty set

for M being Matrix of D

for i being Nat st i in Seg (width M) holds

rng (Col (M,i)) c= Values M

for M being Matrix of D

for i being Nat st i in Seg (width M) holds

rng (Col (M,i)) c= Values M

proof end;

theorem Th13: :: JORDAN1H:13

for D being non empty set

for M being Matrix of D

for i being Nat st i in dom M holds

rng (Line (M,i)) c= Values M

for M being Matrix of D

for i being Nat st i in dom M holds

rng (Line (M,i)) c= Values M

proof end;

theorem Th14: :: JORDAN1H:14

for G being V3() X_increasing-in-column Matrix of (TOP-REAL 2) holds len G <= card (proj1 .: (Values G))

proof end;

theorem Th16: :: JORDAN1H:16

for G being V3() X_equal-in-line X_increasing-in-column Matrix of (TOP-REAL 2) holds len G = card (proj1 .: (Values G))

proof end;

theorem Th17: :: JORDAN1H:17

for G being V3() Y_increasing-in-line Matrix of (TOP-REAL 2) holds width G <= card (proj2 .: (Values G))

proof end;

theorem Th18: :: JORDAN1H:18

for G being V3() Y_equal-in-column Matrix of (TOP-REAL 2) holds card (proj2 .: (Values G)) <= width G

proof end;

theorem Th19: :: JORDAN1H:19

for G being V3() Y_equal-in-column Y_increasing-in-line Matrix of (TOP-REAL 2) holds width G = card (proj2 .: (Values G))

proof end;

theorem :: JORDAN1H:20

for G being Go-board

for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G holds

for k being Nat st 1 <= k & k + 1 <= len f holds

LSeg (f,k) c= left_cell (f,k,G)

for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G holds

for k being Nat st 1 <= k & k + 1 <= len f holds

LSeg (f,k) c= left_cell (f,k,G)

proof end;

theorem :: JORDAN1H:21

for k being Nat

for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f holds

left_cell (f,k,(GoB f)) = left_cell (f,k)

for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f holds

left_cell (f,k,(GoB f)) = left_cell (f,k)

proof end;

theorem Th22: :: JORDAN1H:22

for G being Go-board

for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G holds

for k being Nat st 1 <= k & k + 1 <= len f holds

LSeg (f,k) c= right_cell (f,k,G)

for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G holds

for k being Nat st 1 <= k & k + 1 <= len f holds

LSeg (f,k) c= right_cell (f,k,G)

proof end;

theorem Th23: :: JORDAN1H:23

for k being Nat

for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f holds

right_cell (f,k,(GoB f)) = right_cell (f,k)

for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f holds

right_cell (f,k,(GoB f)) = right_cell (f,k)

proof end;

theorem :: JORDAN1H:24

for P being Subset of (TOP-REAL 2)

for f being non constant standard special_circular_sequence holds

( not P is_a_component_of (L~ f) ` or P = RightComp f or P = LeftComp f )

for f being non constant standard special_circular_sequence holds

( not P is_a_component_of (L~ f) ` or P = RightComp f or P = LeftComp f )

proof end;

theorem :: JORDAN1H:25

for G being Go-board

for f being non constant standard special_circular_sequence st f is_sequence_on G holds

for k being Nat st 1 <= k & k + 1 <= len f holds

( Int (right_cell (f,k,G)) c= RightComp f & Int (left_cell (f,k,G)) c= LeftComp f )

for f being non constant standard special_circular_sequence st f is_sequence_on G holds

for k being Nat st 1 <= k & k + 1 <= len f holds

( Int (right_cell (f,k,G)) c= RightComp f & Int (left_cell (f,k,G)) c= LeftComp f )

proof end;

theorem Th26: :: JORDAN1H:26

for i1, j1, i2, j2 being Nat

for G being Go-board st [i1,j1] in Indices G & [i2,j2] in Indices G & G * (i1,j1) = G * (i2,j2) holds

( i1 = i2 & j1 = j2 )

for G being Go-board st [i1,j1] in Indices G & [i2,j2] in Indices G & G * (i1,j1) = G * (i2,j2) holds

( i1 = i2 & j1 = j2 )

proof end;

theorem Th27: :: JORDAN1H:27

for i1, i2 being Nat

for f being FinSequence of (TOP-REAL 2)

for M being Go-board st f is_sequence_on M holds

mid (f,i1,i2) is_sequence_on M

for f being FinSequence of (TOP-REAL 2)

for M being Go-board st f is_sequence_on M holds

mid (f,i1,i2) is_sequence_on M

proof end;

registration

for b_{1} being Go-board holds

( not b_{1} is empty & b_{1} is non-empty )
end;

cluster non empty-yielding tabular X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column -> non-empty non empty for FinSequence of the carrier of (TOP-REAL 2) * ;

coherence for b

( not b

proof end;

theorem Th28: :: JORDAN1H:28

for i being Nat

for G being Go-board st 1 <= i & i <= len G holds

(SgmX (RealOrd,(proj1 .: (Values G)))) . i = (G * (i,1)) `1

for G being Go-board st 1 <= i & i <= len G holds

(SgmX (RealOrd,(proj1 .: (Values G)))) . i = (G * (i,1)) `1

proof end;

theorem Th29: :: JORDAN1H:29

for j being Nat

for G being Go-board st 1 <= j & j <= width G holds

(SgmX (RealOrd,(proj2 .: (Values G)))) . j = (G * (1,j)) `2

for G being Go-board st 1 <= j & j <= width G holds

(SgmX (RealOrd,(proj2 .: (Values G)))) . j = (G * (1,j)) `2

proof end;

theorem Th30: :: JORDAN1H:30

for f being non empty FinSequence of (TOP-REAL 2)

for G being Go-board st f is_sequence_on G & ex i being Nat st

( [1,i] in Indices G & G * (1,i) in rng f ) & ex i being Nat st

( [(len G),i] in Indices G & G * ((len G),i) in rng f ) holds

proj1 .: (rng f) = proj1 .: (Values G)

for G being Go-board st f is_sequence_on G & ex i being Nat st

( [1,i] in Indices G & G * (1,i) in rng f ) & ex i being Nat st

( [(len G),i] in Indices G & G * ((len G),i) in rng f ) holds

proj1 .: (rng f) = proj1 .: (Values G)

proof end;

theorem Th31: :: JORDAN1H:31

for f being non empty FinSequence of (TOP-REAL 2)

for G being Go-board st f is_sequence_on G & ex i being Nat st

( [i,1] in Indices G & G * (i,1) in rng f ) & ex i being Nat st

( [i,(width G)] in Indices G & G * (i,(width G)) in rng f ) holds

proj2 .: (rng f) = proj2 .: (Values G)

for G being Go-board st f is_sequence_on G & ex i being Nat st

( [i,1] in Indices G & G * (i,1) in rng f ) & ex i being Nat st

( [i,(width G)] in Indices G & G * (i,(width G)) in rng f ) holds

proj2 .: (rng f) = proj2 .: (Values G)

proof end;

registration
end;

theorem Th32: :: JORDAN1H:32

for G being Go-board holds G = GoB ((SgmX (RealOrd,(proj1 .: (Values G)))),(SgmX (RealOrd,(proj2 .: (Values G)))))

proof end;

theorem Th33: :: JORDAN1H:33

for f being non empty FinSequence of (TOP-REAL 2)

for G being Go-board st proj1 .: (rng f) = proj1 .: (Values G) & proj2 .: (rng f) = proj2 .: (Values G) holds

G = GoB f

for G being Go-board st proj1 .: (rng f) = proj1 .: (Values G) & proj2 .: (rng f) = proj2 .: (Values G) holds

G = GoB f

proof end;

theorem Th34: :: JORDAN1H:34

for f being non empty FinSequence of (TOP-REAL 2)

for G being Go-board st f is_sequence_on G & ex i being Nat st

( [1,i] in Indices G & G * (1,i) in rng f ) & ex i being Nat st

( [i,1] in Indices G & G * (i,1) in rng f ) & ex i being Nat st

( [(len G),i] in Indices G & G * ((len G),i) in rng f ) & ex i being Nat st

( [i,(width G)] in Indices G & G * (i,(width G)) in rng f ) holds

G = GoB f

for G being Go-board st f is_sequence_on G & ex i being Nat st

( [1,i] in Indices G & G * (1,i) in rng f ) & ex i being Nat st

( [i,1] in Indices G & G * (i,1) in rng f ) & ex i being Nat st

( [(len G),i] in Indices G & G * ((len G),i) in rng f ) & ex i being Nat st

( [i,(width G)] in Indices G & G * (i,(width G)) in rng f ) holds

G = GoB f

proof end;

theorem Th36: :: JORDAN1H:36

for m, i, n being Nat

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 1 <= i & i + 1 <= len (Gauge (C,n)) holds

( 1 <= [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & [\(((i - 2) / (2 |^ (n -' m))) + 2)/] + 1 <= len (Gauge (C,m)) )

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 1 <= i & i + 1 <= len (Gauge (C,n)) holds

( 1 <= [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & [\(((i - 2) / (2 |^ (n -' m))) + 2)/] + 1 <= len (Gauge (C,m)) )

proof end;

theorem Th37: :: JORDAN1H:37

for m, j, i, n being Nat

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 1 <= i & i + 1 <= len (Gauge (C,n)) & 1 <= j & j + 1 <= width (Gauge (C,n)) holds

ex i1, j1 being Nat st

( i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & j1 = [\(((j - 2) / (2 |^ (n -' m))) + 2)/] & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) )

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 1 <= i & i + 1 <= len (Gauge (C,n)) & 1 <= j & j + 1 <= width (Gauge (C,n)) holds

ex i1, j1 being Nat st

( i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & j1 = [\(((j - 2) / (2 |^ (n -' m))) + 2)/] & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) )

proof end;

theorem Th38: :: JORDAN1H:38

for m, j, i, n being Nat

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 1 <= i & i + 1 <= len (Gauge (C,n)) & 1 <= j & j + 1 <= width (Gauge (C,n)) holds

ex i1, j1 being Nat st

( 1 <= i1 & i1 + 1 <= len (Gauge (C,m)) & 1 <= j1 & j1 + 1 <= width (Gauge (C,m)) & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) )

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 1 <= i & i + 1 <= len (Gauge (C,n)) & 1 <= j & j + 1 <= width (Gauge (C,n)) holds

ex i1, j1 being Nat st

( 1 <= i1 & i1 + 1 <= len (Gauge (C,m)) & 1 <= j1 & j1 + 1 <= width (Gauge (C,m)) & cell ((Gauge (C,n)),i,j) c= cell ((Gauge (C,m)),i1,j1) )

proof end;

theorem Th40: :: JORDAN1H:40

for p being Point of (TOP-REAL 2)

for f being non constant standard special_circular_sequence st Rotate (f,p) is clockwise_oriented holds

f is clockwise_oriented

for f being non constant standard special_circular_sequence st Rotate (f,p) is clockwise_oriented holds

f is clockwise_oriented

proof end;

theorem :: JORDAN1H:41

for f being non constant standard special_circular_sequence st LeftComp f = UBD (L~ f) holds

f is clockwise_oriented

f is clockwise_oriented

proof end;

theorem Th44: :: JORDAN1H:44

for n being Nat

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected holds

GoB (Cage (C,n)) = Gauge (C,n)

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected holds

GoB (Cage (C,n)) = Gauge (C,n)

proof end;

theorem :: JORDAN1H:45

for n being Nat

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected holds

N-min C in right_cell ((Cage (C,n)),1)

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected holds

N-min C in right_cell ((Cage (C,n)),1)

proof end;

theorem Th46: :: JORDAN1H:46

for j, i being Nat

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected & i <= j holds

L~ (Cage (C,j)) c= Cl (RightComp (Cage (C,i)))

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected & i <= j holds

L~ (Cage (C,j)) c= Cl (RightComp (Cage (C,i)))

proof end;

theorem Th47: :: JORDAN1H:47

for j, i being Nat

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected & i <= j holds

LeftComp (Cage (C,i)) c= LeftComp (Cage (C,j))

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected & i <= j holds

LeftComp (Cage (C,i)) c= LeftComp (Cage (C,j))

proof end;

theorem :: JORDAN1H:48

for j, i being Nat

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected & i <= j holds

RightComp (Cage (C,j)) c= RightComp (Cage (C,i))

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected & i <= j holds

RightComp (Cage (C,j)) c= RightComp (Cage (C,i))

proof end;

definition

let C be compact non horizontal non vertical Subset of (TOP-REAL 2);

let n be Nat;

correctness

coherence

(2 |^ (n -' 1)) + 2 is Nat;

;

end;
let n be Nat;

correctness

coherence

(2 |^ (n -' 1)) + 2 is Nat;

;

:: deftheorem defines X-SpanStart JORDAN1H:def 2 :

for C being compact non horizontal non vertical Subset of (TOP-REAL 2)

for n being Nat holds X-SpanStart (C,n) = (2 |^ (n -' 1)) + 2;

for C being compact non horizontal non vertical Subset of (TOP-REAL 2)

for n being Nat holds X-SpanStart (C,n) = (2 |^ (n -' 1)) + 2;

theorem Th49: :: JORDAN1H:49

for n being Nat

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds

( 2 < X-SpanStart (C,n) & X-SpanStart (C,n) < len (Gauge (C,n)) )

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds

( 2 < X-SpanStart (C,n) & X-SpanStart (C,n) < len (Gauge (C,n)) )

proof end;

theorem Th50: :: JORDAN1H:50

for n being Nat

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds

( 1 <= (X-SpanStart (C,n)) -' 1 & (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n)) )

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds

( 1 <= (X-SpanStart (C,n)) -' 1 & (X-SpanStart (C,n)) -' 1 < len (Gauge (C,n)) )

proof end;

definition

let C be compact non horizontal non vertical Subset of (TOP-REAL 2);

let n be Nat;

end;
let n be Nat;

pred n is_sufficiently_large_for C means :: JORDAN1H:def 3

ex j being Nat st

( j < width (Gauge (C,n)) & cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= BDD C );

ex j being Nat st

( j < width (Gauge (C,n)) & cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= BDD C );

:: deftheorem defines is_sufficiently_large_for JORDAN1H:def 3 :

for C being compact non horizontal non vertical Subset of (TOP-REAL 2)

for n being Nat holds

( n is_sufficiently_large_for C iff ex j being Nat st

( j < width (Gauge (C,n)) & cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= BDD C ) );

for C being compact non horizontal non vertical Subset of (TOP-REAL 2)

for n being Nat holds

( n is_sufficiently_large_for C iff ex j being Nat st

( j < width (Gauge (C,n)) & cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= BDD C ) );

theorem :: JORDAN1H:51

for n being Nat

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st n is_sufficiently_large_for C holds

n >= 1

for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st n is_sufficiently_large_for C holds

n >= 1

proof end;

theorem :: JORDAN1H:52

for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)

for n being Nat

for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds

for i1, j1 being Nat st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds

[(i1 -' 1),(j1 + 1)] in Indices (Gauge (C,n))

for n being Nat

for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds

for i1, j1 being Nat st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds

[(i1 -' 1),(j1 + 1)] in Indices (Gauge (C,n))

proof end;

theorem :: JORDAN1H:53

for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)

for n being Nat

for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds

for i1, j1 being Nat st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds

[(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n))

for n being Nat

for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds

for i1, j1 being Nat st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds

[(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n))

proof end;

theorem :: JORDAN1H:54

for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)

for n being Nat

for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds

for j1, i2 being Nat st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds

[i2,(j1 -' 1)] in Indices (Gauge (C,n))

for n being Nat

for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds

for j1, i2 being Nat st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds

[i2,(j1 -' 1)] in Indices (Gauge (C,n))

proof end;

theorem :: JORDAN1H:55

for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)

for n being Nat

for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds

for i1, j2 being Nat st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds

[(i1 + 1),j2] in Indices (Gauge (C,n))

for n being Nat

for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds

for i1, j2 being Nat st left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds

[(i1 + 1),j2] in Indices (Gauge (C,n))

proof end;

theorem :: JORDAN1H:56

for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)

for n being Nat

for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds

for i1, j1 being Nat st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds

[i1,(j1 + 2)] in Indices (Gauge (C,n))

for n being Nat

for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds

for i1, j1 being Nat st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds

[i1,(j1 + 2)] in Indices (Gauge (C,n))

proof end;

theorem :: JORDAN1H:57

for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)

for n being Nat

for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds

for i1, j1 being Nat st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds

[(i1 + 2),j1] in Indices (Gauge (C,n))

for n being Nat

for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds

for i1, j1 being Nat st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds

[(i1 + 2),j1] in Indices (Gauge (C,n))

proof end;

theorem :: JORDAN1H:58

for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)

for n being Nat

for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds

for j1, i2 being Nat st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds

[(i2 -' 1),j1] in Indices (Gauge (C,n))

for n being Nat

for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds

for j1, i2 being Nat st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds

[(i2 -' 1),j1] in Indices (Gauge (C,n))

proof end;

theorem :: JORDAN1H:59

for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)

for n being Nat

for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds

for i1, j2 being Nat st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds

[i1,(j2 -' 1)] in Indices (Gauge (C,n))

for n being Nat

for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds

for i1, j2 being Nat st front_left_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds

[i1,(j2 -' 1)] in Indices (Gauge (C,n))

proof end;

theorem :: JORDAN1H:60

for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)

for n being Nat

for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds

for i1, j1 being Nat st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds

[(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n))

for n being Nat

for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds

for i1, j1 being Nat st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [i1,(j1 + 1)] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,(j1 + 1)) holds

[(i1 + 1),(j1 + 1)] in Indices (Gauge (C,n))

proof end;

theorem :: JORDAN1H:61

for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)

for n being Nat

for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds

for i1, j1 being Nat st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds

[(i1 + 1),(j1 -' 1)] in Indices (Gauge (C,n))

for n being Nat

for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds

for i1, j1 being Nat st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,j1) & [(i1 + 1),j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * ((i1 + 1),j1) holds

[(i1 + 1),(j1 -' 1)] in Indices (Gauge (C,n))

proof end;

theorem :: JORDAN1H:62

for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)

for n being Nat

for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds

for j1, i2 being Nat st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds

[i2,(j1 + 1)] in Indices (Gauge (C,n))

for n being Nat

for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds

for j1, i2 being Nat st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [(i2 + 1),j1] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * ((i2 + 1),j1) & [i2,j1] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i2,j1) holds

[i2,(j1 + 1)] in Indices (Gauge (C,n))

proof end;

theorem :: JORDAN1H:63

for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)

for n being Nat

for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds

for i1, j2 being Nat st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds

[(i1 -' 1),j2] in Indices (Gauge (C,n))

for n being Nat

for f being FinSequence of (TOP-REAL 2) st f is_sequence_on Gauge (C,n) & len f > 1 holds

for i1, j2 being Nat st front_right_cell (f,((len f) -' 1),(Gauge (C,n))) meets C & [i1,(j2 + 1)] in Indices (Gauge (C,n)) & f /. ((len f) -' 1) = (Gauge (C,n)) * (i1,(j2 + 1)) & [i1,j2] in Indices (Gauge (C,n)) & f /. (len f) = (Gauge (C,n)) * (i1,j2) holds

[(i1 -' 1),j2] in Indices (Gauge (C,n))

proof end;