:: JORDAN1E semantic presentation

begin

theorem Th1: :: JORDAN1E:1
for f, g being FinSequence of (TOP-REAL 2) st f is_in_the_area_of g holds
for p being Element of (TOP-REAL 2) st p in rng f holds
f -: p is_in_the_area_of g
proof
let f, g be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_in_the_area_of g implies for p being Element of (TOP-REAL 2) st p in rng f holds
f -: p is_in_the_area_of g )
assume A1: f is_in_the_area_of g ; ::_thesis: for p being Element of (TOP-REAL 2) st p in rng f holds
f -: p is_in_the_area_of g
let p be Element of (TOP-REAL 2); ::_thesis: ( p in rng f implies f -: p is_in_the_area_of g )
assume A2: p in rng f ; ::_thesis: f -: p is_in_the_area_of g
then A3: p .. f <= len f by FINSEQ_4:21;
let n be Element of NAT ; :: according to SPRECT_2:def_1 ::_thesis: ( not n in dom (f -: p) or ( W-bound (L~ g) <= ((f -: p) /. n) `1 & ((f -: p) /. n) `1 <= E-bound (L~ g) & S-bound (L~ g) <= ((f -: p) /. n) `2 & ((f -: p) /. n) `2 <= N-bound (L~ g) ) )
assume A4: n in dom (f -: p) ; ::_thesis: ( W-bound (L~ g) <= ((f -: p) /. n) `1 & ((f -: p) /. n) `1 <= E-bound (L~ g) & S-bound (L~ g) <= ((f -: p) /. n) `2 & ((f -: p) /. n) `2 <= N-bound (L~ g) )
A5: len (f -: p) = p .. f by A2, FINSEQ_5:42;
then  n in Seg (p .. f) by A4, FINSEQ_1:def_3;
then A6: (f -: p) /. n = f /. n by A2, FINSEQ_5:43;
A7: n in Seg (len (f -: p)) by A4, FINSEQ_1:def_3;
then  n <= p .. f by A5, FINSEQ_1:1;
then A8: n <= len f by A3, XXREAL_0:2;
 1 <= n by A7, FINSEQ_1:1;
then  n in dom f by A8, FINSEQ_3:25;
hence  ( W-bound (L~ g) <= ((f -: p) /. n) `1 & ((f -: p) /. n) `1 <= E-bound (L~ g) & S-bound (L~ g) <= ((f -: p) /. n) `2 & ((f -: p) /. n) `2 <= N-bound (L~ g) ) by A1, A6, SPRECT_2:def_1; ::_thesis: verum
end;

theorem Th2: :: JORDAN1E:2
for f, g being FinSequence of (TOP-REAL 2) st f is_in_the_area_of g holds
for p being Element of (TOP-REAL 2) st p in rng f holds
f :- p is_in_the_area_of g
proof
let f, g be FinSequence of (TOP-REAL 2); ::_thesis: ( f is_in_the_area_of g implies for p being Element of (TOP-REAL 2) st p in rng f holds
f :- p is_in_the_area_of g )
assume A1: f is_in_the_area_of g ; ::_thesis: for p being Element of (TOP-REAL 2) st p in rng f holds
f :- p is_in_the_area_of g
let p be Element of (TOP-REAL 2); ::_thesis: ( p in rng f implies f :- p is_in_the_area_of g )
assume A2: p in rng f ; ::_thesis: f :- p is_in_the_area_of g
let n be Element of NAT ; :: according to SPRECT_2:def_1 ::_thesis: ( not n in dom (f :- p) or ( W-bound (L~ g) <= ((f :- p) /. n) `1 & ((f :- p) /. n) `1 <= E-bound (L~ g) & S-bound (L~ g) <= ((f :- p) /. n) `2 & ((f :- p) /. n) `2 <= N-bound (L~ g) ) )
 1 <= p .. f by A2, FINSEQ_4:21;
then A3: 0 + 1 <= (n -' 1) + (p .. f) by XREAL_1:7;
assume A4: n in dom (f :- p) ; ::_thesis: ( W-bound (L~ g) <= ((f :- p) /. n) `1 & ((f :- p) /. n) `1 <= E-bound (L~ g) & S-bound (L~ g) <= ((f :- p) /. n) `2 & ((f :- p) /. n) `2 <= N-bound (L~ g) )
then A5: n in Seg (len (f :- p)) by FINSEQ_1:def_3;
then A6: 0 + 1 <= n by FINSEQ_1:1;
then  (n -' 1) + 1 = n by XREAL_1:235;
then A7: (f :- p) /. n = f /. ((n -' 1) + (p .. f)) by A2, A4, FINSEQ_5:52;
 len (f :- p) = ((len f) - (p .. f)) + 1 by A2, FINSEQ_5:50;
then  n <= ((len f) - (p .. f)) + 1 by A5, FINSEQ_1:1;
then  n - 1 <= (len f) - (p .. f) by XREAL_1:20;
then A8: (n - 1) + (p .. f) <= len f by XREAL_1:19;
 n - 1 >= 0 by A6, XREAL_1:19;
then  (n -' 1) + (p .. f) <= len f by A8, XREAL_0:def_2;
then  (n -' 1) + (p .. f) in dom f by A3, FINSEQ_3:25;
hence  ( W-bound (L~ g) <= ((f :- p) /. n) `1 & ((f :- p) /. n) `1 <= E-bound (L~ g) & S-bound (L~ g) <= ((f :- p) /. n) `2 & ((f :- p) /. n) `2 <= N-bound (L~ g) ) by A1, A7, SPRECT_2:def_1; ::_thesis: verum
end;

theorem :: JORDAN1E:3
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in L~ f holds
L_Cut (f,p) <> {}
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st p in L~ f holds
L_Cut (f,p) <> {}
let p be Point of (TOP-REAL 2); ::_thesis: ( p in L~ f implies L_Cut (f,p) <> {} )
assume that
A1: p in L~ f and
A2: L_Cut (f,p) = {} ; ::_thesis: contradiction
 len f <> 0 by A1, TOPREAL1:22;
then  f <> {} ;
then A3: len f in dom f by FINSEQ_5:6;
A4: ( p <> f . ((Index (p,f)) + 1) or p = f . ((Index (p,f)) + 1) ) ;
 not <*p*> ^ (mid (f,((Index (p,f)) + 1),(len f))) is empty ;
then  L_Cut (f,p) = mid (f,((Index (p,f)) + 1),(len f)) by A2, A4, JORDAN3:def_3;
then  not (Index (p,f)) + 1 in dom f by A2, A3, SPRECT_2:7;
then  ( (Index (p,f)) + 1 < 1 or (Index (p,f)) + 1 > len f ) by FINSEQ_3:25;
then  Index (p,f) >= len f by NAT_1:11, NAT_1:13;
hence  contradiction by A1, JORDAN3:8; ::_thesis: verum
end;

theorem :: JORDAN1E:4
for f being FinSequence of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p in L~ f & len (R_Cut (f,p)) >= 2 holds
f . 1 in L~ (R_Cut (f,p))
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: for p being Point of (TOP-REAL 2) st p in L~ f & len (R_Cut (f,p)) >= 2 holds
f . 1 in L~ (R_Cut (f,p))
let p be Point of (TOP-REAL 2); ::_thesis: ( p in L~ f & len (R_Cut (f,p)) >= 2 implies f . 1 in L~ (R_Cut (f,p)) )
assume A1: p in L~ f ; ::_thesis: ( not len (R_Cut (f,p)) >= 2 or f . 1 in L~ (R_Cut (f,p)) )
then  len f <> 0 by TOPREAL1:22;
then  len f > 0 by NAT_1:3;
then  0 + 1 <= len f by NAT_1:13;
then A2: (R_Cut (f,p)) . 1 = f . 1 by A1, JORDAN1B:3;
assume  2 <= len (R_Cut (f,p)) ; ::_thesis: f . 1 in L~ (R_Cut (f,p))
hence  f . 1 in L~ (R_Cut (f,p)) by A2, JORDAN3:1; ::_thesis: verum
end;

theorem Th5: :: JORDAN1E:5
for f being FinSequence of (TOP-REAL 2) st f is being_S-Seq holds
for p being Point of (TOP-REAL 2) st p in L~ f holds
not f . 1 in L~ (mid (f,((Index (p,f)) + 1),(len f)))
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is being_S-Seq implies for p being Point of (TOP-REAL 2) st p in L~ f holds
not f . 1 in L~ (mid (f,((Index (p,f)) + 1),(len f))) )
assume A1: f is being_S-Seq ; ::_thesis: for p being Point of (TOP-REAL 2) st p in L~ f holds
not f . 1 in L~ (mid (f,((Index (p,f)) + 1),(len f)))
let p be Point of (TOP-REAL 2); ::_thesis: ( p in L~ f implies not f . 1 in L~ (mid (f,((Index (p,f)) + 1),(len f))) )
assume that
A2: p in L~ f and
A3: f . 1 in L~ (mid (f,((Index (p,f)) + 1),(len f))) ; ::_thesis: contradiction
 len f <> 0 by A2, TOPREAL1:22;
then  f <> {} ;
then  1 in dom f by FINSEQ_5:6;
then A4: f /. 1 in L~ (mid (f,((Index (p,f)) + 1),(len f))) by A3, PARTFUN1:def_6;
 Index (p,f) < len f by A2, JORDAN3:8;
then  (Index (p,f)) + 1 <= len f by NAT_1:13;
then  (Index (p,f)) + 1 = 0 + 1 by A1, A4, JORDAN5B:16, NAT_1:11;
hence  contradiction by A2, JORDAN3:8; ::_thesis: verum
end;

theorem Th6: :: JORDAN1E:6
for i, j, m, n being Element of NAT st i + j = m + n & i <= m & j <= n holds
i = m
proof
let i, j, m, n be Element of NAT ; ::_thesis: ( i + j = m + n & i <= m & j <= n implies i = m )
assume that
A1: i + j = m + n and
A2: i <= m and
A3: j <= n ; ::_thesis: i = m
consider k being Nat such that
A4: m = i + k by A2, NAT_1:10;
consider l being Nat such that
A5: n = j + l by A3, NAT_1:10;
 j + (l + k) = j + 0 by A1, A4, A5;
then  k = 0 by NAT_1:7;
hence  i = m by A4; ::_thesis: verum
end;

theorem :: JORDAN1E:7
for f being FinSequence of (TOP-REAL 2) st f is being_S-Seq holds
for p being Point of (TOP-REAL 2) st p in L~ f & f . 1 in L~ (L_Cut (f,p)) holds
f . 1 = p
proof
let f be FinSequence of (TOP-REAL 2); ::_thesis: ( f is being_S-Seq implies for p being Point of (TOP-REAL 2) st p in L~ f & f . 1 in L~ (L_Cut (f,p)) holds
f . 1 = p )
assume A1: f is being_S-Seq ; ::_thesis: for p being Point of (TOP-REAL 2) st p in L~ f & f . 1 in L~ (L_Cut (f,p)) holds
f . 1 = p
then A2: len f >= 2 by TOPREAL1:def_8;
A3: len f in dom f by A1, FINSEQ_5:6;
 1 in dom f by A1, FINSEQ_5:6;
then A4: f /. 1 = f . 1 by PARTFUN1:def_6;
let p be Point of (TOP-REAL 2); ::_thesis: ( p in L~ f & f . 1 in L~ (L_Cut (f,p)) implies f . 1 = p )
assume that
A5: p in L~ f and
A6: f . 1 in L~ (L_Cut (f,p)) and
A7: f . 1 <> p ; ::_thesis: contradiction
set g = mid (f,((Index (p,f)) + 1),(len f));
A8: not f . 1 in L~ (mid (f,((Index (p,f)) + 1),(len f))) by A1, A5, Th5;
then  p <> f . ((Index (p,f)) + 1) by A6, JORDAN3:def_3;
then A9: L_Cut (f,p) = <*p*> ^ (mid (f,((Index (p,f)) + 1),(len f))) by JORDAN3:def_3;
percases ( mid (f,((Index (p,f)) + 1),(len f)) is empty or not mid (f,((Index (p,f)) + 1),(len f)) is empty ) ;
suppose mid (f,((Index (p,f)) + 1),(len f)) is empty ; ::_thesis: contradiction
then  L_Cut (f,p) = <*p*> by A9, FINSEQ_1:34;
then  len (L_Cut (f,p)) = 1 by FINSEQ_1:39;
hence  contradiction by A6, TOPREAL1:22; ::_thesis: verum
end;
suppose not mid (f,((Index (p,f)) + 1),(len f)) is empty ; ::_thesis: contradiction
then  L~ (L_Cut (f,p)) = (LSeg (p,((mid (f,((Index (p,f)) + 1),(len f))) /. 1))) \/ (L~ (mid (f,((Index (p,f)) + 1),(len f)))) by A9, SPPOL_2:20;
then A10: f . 1 in LSeg (p,((mid (f,((Index (p,f)) + 1),(len f))) /. 1)) by A6, A8, XBOOLE_0:def_3;
A11: 1 + 1 <= len f by A1, TOPREAL1:def_8;
then A12: 2 in dom f by FINSEQ_3:25;
consider i being Element of NAT  such that
A13: 1 <= i and
A14: i + 1 <= len (<*p*> ^ (mid (f,((Index (p,f)) + 1),(len f)))) and
A15: f /. 1 in LSeg ((<*p*> ^ (mid (f,((Index (p,f)) + 1),(len f)))),i) by A6, A4, A9, SPPOL_2:13;
 LSeg ((<*p*> ^ (mid (f,((Index (p,f)) + 1),(len f)))),i) c= LSeg (f,(((Index (p,f)) + i) -' 1)) by A5, A13, A14, JORDAN3:16;
then A16: ((Index (p,f)) + i) -' 1 = 1 by A1, A2, A15, JORDAN5B:30;
A17: 1 <= Index (p,f) by A5, JORDAN3:8;
then  1 + 1 <= (Index (p,f)) + i by A13, XREAL_1:7;
then A18: (Index (p,f)) + i = 1 + 1 by A16, XREAL_1:235, XXREAL_0:2;
then  Index (p,f) = 1 by A13, A17, Th6;
then  p in LSeg (f,1) by A5, JORDAN3:9;
then A19: p in LSeg ((f /. 1),(f /. (1 + 1))) by A11, TOPREAL1:def_3;
 i = 1 by A13, A17, A18, Th6;
then  (mid (f,((Index (p,f)) + 1),(len f))) /. 1 = f /. (1 + 1) by A3, A18, A12, SPRECT_2:8;
hence  contradiction by A7, A4, A10, A19, SPRECT_3:6; ::_thesis: verum
end;
end;
end;

begin

definition
let C be compact non horizontal non vertical Subset of (TOP-REAL 2);
let n be Nat;
func Upper_Seq (C,n) ->  FinSequence of (TOP-REAL 2) equals :: JORDAN1E:def 1
(Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n))));
coherence
 (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n)))) is FinSequence of (TOP-REAL 2) ;
end;

:: deftheorem  defines Upper_Seq JORDAN1E:def_1_:_
 for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds Upper_Seq (C,n) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n))));

theorem Th8: :: JORDAN1E:8
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds len (Upper_Seq (C,n)) = (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))
proof
let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Nat holds len (Upper_Seq (C,n)) = (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))
let n be Nat; ::_thesis: len (Upper_Seq (C,n)) = (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))
 E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;
then  E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:90, SPRECT_2:43;
hence  len (Upper_Seq (C,n)) = (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_5:42; ::_thesis: verum
end;

definition
let C be compact non horizontal non vertical Subset of (TOP-REAL 2);
let n be Nat;
func Lower_Seq (C,n) ->  FinSequence of (TOP-REAL 2) equals :: JORDAN1E:def 2
(Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n))));
coherence
 (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n)))) is FinSequence of (TOP-REAL 2) ;
end;

:: deftheorem  defines Lower_Seq JORDAN1E:def_2_:_
 for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds Lower_Seq (C,n) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n))));

theorem Th9: :: JORDAN1E:9
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Nat holds len (Lower_Seq (C,n)) = ((len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1
proof
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Nat holds len (Lower_Seq (C,n)) = ((len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1
let n be Nat; ::_thesis: len (Lower_Seq (C,n)) = ((len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1
 E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;
then  E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:90, SPRECT_2:43;
hence  len (Lower_Seq (C,n)) = ((len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 by FINSEQ_5:50; ::_thesis: verum
end;

registration
let C be compact non horizontal non vertical Subset of (TOP-REAL 2);
let n be Nat;
cluster Upper_Seq (C,n) ->  non empty ;
coherence
 not Upper_Seq (C,n) is empty
proof
 E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;
then A1: E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:90, SPRECT_2:43;
 len (Upper_Seq (C,n)) = (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by Th8;
hence  not Upper_Seq (C,n) is empty by A1, FINSEQ_4:21; ::_thesis: verum
end;
cluster Lower_Seq (C,n) ->  non empty ;
coherence
 not Lower_Seq (C,n) is empty
proof
 E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;
then A2: E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:90, SPRECT_2:43;
 len (Lower_Seq (C,n)) = ((len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 by Th9;
then  ((len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - (len (Lower_Seq (C,n)))) + 1 <= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A2, FINSEQ_4:21;
then  (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - (len (Lower_Seq (C,n))) <= (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - 1 by XREAL_1:19;
hence  not Lower_Seq (C,n) is empty by XREAL_1:10; ::_thesis: verum
end;
end;

registration
let C be compact non horizontal non vertical Subset of (TOP-REAL 2);
let n be Element of NAT ;
cluster Upper_Seq (C,n) ->  one-to-one special unfolded s.n.c. ;
coherence
 ( Upper_Seq (C,n) is one-to-one & Upper_Seq (C,n) is special & Upper_Seq (C,n) is unfolded & Upper_Seq (C,n) is s.n.c. )
proof
set f = Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))));
A1: W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:43;
 E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;
then A2: E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:90, SPRECT_2:43;
A3: len (Upper_Seq (C,n)) = (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by Th8;
now__::_thesis:_for_i1,_j1_being_set_st_i1_in_dom_(Upper_Seq_(C,n))_&_j1_in_dom_(Upper_Seq_(C,n))_&_(Upper_Seq_(C,n))_._i1_=_(Upper_Seq_(C,n))_._j1_holds_
not_i1_<>_j1
let i1, j1 be set ; ::_thesis: ( i1 in dom (Upper_Seq (C,n)) & j1 in dom (Upper_Seq (C,n)) & (Upper_Seq (C,n)) . i1 = (Upper_Seq (C,n)) . j1 implies not i1 <> j1 )
assume that
A4: i1 in dom (Upper_Seq (C,n)) and
A5: j1 in dom (Upper_Seq (C,n)) and
A6: (Upper_Seq (C,n)) . i1 = (Upper_Seq (C,n)) . j1 and
A7: i1 <> j1 ; ::_thesis: contradiction
reconsider i2 = i1, j2 = j1 as Element of NAT by A4, A5;
A8: i2 in Seg ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A3, A4, FINSEQ_1:def_3;
then A9: 1 <= i2 by FINSEQ_1:1;
A10: L~ (Cage (C,n)) = L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by REVROT_1:33;
A11: j2 in Seg ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A3, A5, FINSEQ_1:def_3;
then A12: 1 <= j2 by FINSEQ_1:1;
 j2 <= (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A11, FINSEQ_1:1;
then A13: j2 < len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A10, SPRECT_5:16, XXREAL_0:2;
A14: (Upper_Seq (C,n)) . j1 = (Upper_Seq (C,n)) /. j2 by A5, PARTFUN1:def_6
.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. j2 by A2, A11, FINSEQ_5:43 ;
 i2 <= (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A8, FINSEQ_1:1;
then A15: i2 < len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A10, SPRECT_5:16, XXREAL_0:2;
A16: (Upper_Seq (C,n)) . i1 = (Upper_Seq (C,n)) /. i2 by A4, PARTFUN1:def_6
.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. i2 by A2, A8, FINSEQ_5:43 ;
percases ( i2 < j2 or j2 < i2 ) by A7, XXREAL_0:1;
suppose i2 < j2 ; ::_thesis: contradiction
hence  contradiction by A6, A16, A14, A9, A13, GOBOARD7:36; ::_thesis: verum
end;
suppose j2 < i2 ; ::_thesis: contradiction
hence  contradiction by A6, A16, A14, A12, A15, GOBOARD7:36; ::_thesis: verum
end;
end;
end;
hence  Upper_Seq (C,n) is one-to-one by FUNCT_1:def_4; ::_thesis: ( Upper_Seq (C,n) is special & Upper_Seq (C,n) is unfolded & Upper_Seq (C,n) is s.n.c. )
thus  Upper_Seq (C,n) is special ; ::_thesis: ( Upper_Seq (C,n) is unfolded & Upper_Seq (C,n) is s.n.c. )
thus  Upper_Seq (C,n) is unfolded ; ::_thesis: Upper_Seq (C,n) is s.n.c.
let i, j be Nat; :: according to TOPREAL1:def_7 ::_thesis: ( j <= i + 1 or LSeg ((Upper_Seq (C,n)),i) misses LSeg ((Upper_Seq (C,n)),j) )
assume A17: i + 1 < j ; ::_thesis: LSeg ((Upper_Seq (C,n)),i) misses LSeg ((Upper_Seq (C,n)),j)
 len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) > 0 by NAT_1:3;
then  0 + 1 <= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by NAT_1:13;
then A18: len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) in dom (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_3:25;
A19: ( i in NAT & j in NAT ) by ORDINAL1:def_12;
now__::_thesis:_LSeg_((Upper_Seq_(C,n)),i)_misses_LSeg_((Upper_Seq_(C,n)),j)
percases ( j + 1 <= len (Upper_Seq (C,n)) or j + 1 > len (Upper_Seq (C,n)) ) ;
supposeA20: j + 1 <= len (Upper_Seq (C,n)) ; ::_thesis: LSeg ((Upper_Seq (C,n)),i) misses LSeg ((Upper_Seq (C,n)),j)
A21: (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) <= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A2, FINSEQ_4:21;
A22: j + 1 <= (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A2, A20, FINSEQ_5:42;
A23: now__::_thesis:_j_+_1_<_len_(Rotate_((Cage_(C,n)),(W-min_(L~_(Cage_(C,n))))))
percases ( j + 1 < (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) or j + 1 = (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) ) by A22, XXREAL_0:1;
suppose j + 1 < (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) ; ::_thesis: j + 1 < len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))
hence  j + 1 < len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A21, XXREAL_0:2; ::_thesis: verum
end;
supposeA24: j + 1 = (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) ; ::_thesis: not j + 1 >= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))
assume  j + 1 >= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) ; ::_thesis: contradiction
then  (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) = len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A21, A24, XXREAL_0:1;
then  E-max (L~ (Cage (C,n))) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) . (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A2, FINSEQ_4:19
.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A18, PARTFUN1:def_6
.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1 by FINSEQ_6:def_1
.= W-min (L~ (Cage (C,n))) by A1, FINSEQ_6:92 ;
hence  contradiction by TOPREAL5:19; ::_thesis: verum
end;
end;
end;
 j < len (Upper_Seq (C,n)) by A20, NAT_1:13;
then A25: LSeg ((Upper_Seq (C,n)),i) = LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),i) by A17, SPPOL_2:9, XXREAL_0:2;
 LSeg ((Upper_Seq (C,n)),j) = LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),j) by A20, SPPOL_2:9;
hence  LSeg ((Upper_Seq (C,n)),i) misses LSeg ((Upper_Seq (C,n)),j) by A17, A19, A25, A23, GOBOARD5:def_4; ::_thesis: verum
end;
suppose j + 1 > len (Upper_Seq (C,n)) ; ::_thesis: LSeg ((Upper_Seq (C,n)),i) misses LSeg ((Upper_Seq (C,n)),j)
then  LSeg ((Upper_Seq (C,n)),j) = {} by TOPREAL1:def_3;
then  (LSeg ((Upper_Seq (C,n)),i)) /\ (LSeg ((Upper_Seq (C,n)),j)) = {} ;
hence  LSeg ((Upper_Seq (C,n)),i) misses LSeg ((Upper_Seq (C,n)),j) by XBOOLE_0:def_7; ::_thesis: verum
end;
end;
end;
hence  LSeg ((Upper_Seq (C,n)),i) misses LSeg ((Upper_Seq (C,n)),j) ; ::_thesis: verum
end;
cluster Lower_Seq (C,n) ->  one-to-one special unfolded s.n.c. ;
coherence
 ( Lower_Seq (C,n) is one-to-one & Lower_Seq (C,n) is special & Lower_Seq (C,n) is unfolded & Lower_Seq (C,n) is s.n.c. )
proof
set f = Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))));
A26: L~ (Cage (C,n)) = L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by REVROT_1:33;
 W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:43;
then A27: (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1 = W-min (L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A26, FINSEQ_6:92;
then  (W-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) <= (N-min (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A26, SPRECT_5:23;
then  (N-min (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) > 1 by A26, A27, SPRECT_5:22, XXREAL_0:2;
then  (N-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) > 1 by A26, A27, SPRECT_5:24, XXREAL_0:2;
then A28: (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) > 1 by A26, A27, SPRECT_5:25, XXREAL_0:2;
 E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;
then A29: E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:90, SPRECT_2:43;
A30: len (Lower_Seq (C,n)) = ((len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 by Th9;
now__::_thesis:_for_i1,_j1_being_set_st_i1_in_dom_(Lower_Seq_(C,n))_&_j1_in_dom_(Lower_Seq_(C,n))_&_(Lower_Seq_(C,n))_._i1_=_(Lower_Seq_(C,n))_._j1_holds_
not_i1_<>_j1
let i1, j1 be set ; ::_thesis: ( i1 in dom (Lower_Seq (C,n)) & j1 in dom (Lower_Seq (C,n)) & (Lower_Seq (C,n)) . i1 = (Lower_Seq (C,n)) . j1 implies not i1 <> j1 )
assume that
A31: i1 in dom (Lower_Seq (C,n)) and
A32: j1 in dom (Lower_Seq (C,n)) and
A33: (Lower_Seq (C,n)) . i1 = (Lower_Seq (C,n)) . j1 and
A34: i1 <> j1 ; ::_thesis: contradiction
reconsider i2 = i1, j2 = j1 as Element of NAT by A31, A32;
A35: i2 in Seg (len (Lower_Seq (C,n))) by A31, FINSEQ_1:def_3;
then  i2 >= 1 by FINSEQ_1:1;
then A36: i2 = (i2 -' 1) + 1 by XREAL_1:235;
A37: (Lower_Seq (C,n)) . i1 = (Lower_Seq (C,n)) /. i2 by A31, PARTFUN1:def_6
.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. ((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) by A29, A31, A36, FINSEQ_5:52 ;
A38: j2 in Seg (len (Lower_Seq (C,n))) by A32, FINSEQ_1:def_3;
then  j2 >= 1 by FINSEQ_1:1;
then A39: j2 = (j2 -' 1) + 1 by XREAL_1:235;
A40: (Lower_Seq (C,n)) . j1 = (Lower_Seq (C,n)) /. j2 by A32, PARTFUN1:def_6
.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. ((j2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) by A29, A32, A39, FINSEQ_5:52 ;
 0 + 1 <= i2 by A35, FINSEQ_1:1;
then A41: i2 - 1 >= 0 by XREAL_1:19;
 i2 <= ((len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 by A30, A35, FINSEQ_1:1;
then  i2 - 1 <= (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by XREAL_1:20;
then  (i2 - 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) <= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by XREAL_1:19;
then A42: (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) <= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A41, XREAL_0:def_2;
 0 + 1 <= j2 by A38, FINSEQ_1:1;
then A43: j2 - 1 >= 0 by XREAL_1:19;
 j2 <= ((len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 by A30, A38, FINSEQ_1:1;
then  j2 - 1 <= (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by XREAL_1:20;
then  (j2 - 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) <= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by XREAL_1:19;
then A44: (j2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) <= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A43, XREAL_0:def_2;
 (j2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) >= (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by NAT_1:11;
then A45: 1 < (j2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A28, XXREAL_0:2;
 (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) >= (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by NAT_1:11;
then A46: 1 < (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A28, XXREAL_0:2;
percases ( i2 < j2 or j2 < i2 ) by A34, XXREAL_0:1;
suppose i2 < j2 ; ::_thesis: contradiction
then  i2 - 1 < j2 - 1 by XREAL_1:9;
then  i2 - 1 < j2 -' 1 by XREAL_0:def_2;
then  i2 -' 1 < j2 -' 1 by A41, XREAL_0:def_2;
then  (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) < (j2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by XREAL_1:6;
hence  contradiction by A33, A37, A40, A44, A46, GOBOARD7:37; ::_thesis: verum
end;
suppose j2 < i2 ; ::_thesis: contradiction
then  j2 - 1 < i2 - 1 by XREAL_1:9;
then  j2 - 1 < i2 -' 1 by XREAL_0:def_2;
then  j2 -' 1 < i2 -' 1 by A43, XREAL_0:def_2;
then  (j2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) < (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by XREAL_1:6;
hence  contradiction by A33, A37, A40, A42, A45, GOBOARD7:37; ::_thesis: verum
end;
end;
end;
hence  Lower_Seq (C,n) is one-to-one by FUNCT_1:def_4; ::_thesis: ( Lower_Seq (C,n) is special & Lower_Seq (C,n) is unfolded & Lower_Seq (C,n) is s.n.c. )
 E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;
then A47: E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:90, SPRECT_2:43;
hence  Lower_Seq (C,n) is special by SPPOL_2:39; ::_thesis: ( Lower_Seq (C,n) is unfolded & Lower_Seq (C,n) is s.n.c. )
thus  Lower_Seq (C,n) is unfolded by A47, SPPOL_2:27; ::_thesis: Lower_Seq (C,n) is s.n.c.
let i, j be Nat; :: according to TOPREAL1:def_7 ::_thesis: ( j <= i + 1 or LSeg ((Lower_Seq (C,n)),i) misses LSeg ((Lower_Seq (C,n)),j) )
assume A48: i + 1 < j ; ::_thesis: LSeg ((Lower_Seq (C,n)),i) misses LSeg ((Lower_Seq (C,n)),j)
 i + 1 >= 1 by NAT_1:11;
then  j = (j -' 1) + 1 by A48, XREAL_1:235, XXREAL_0:2;
then A49: LSeg ((Lower_Seq (C,n)),j) = LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),((j -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))))) by A47, SPPOL_2:10;
now__::_thesis:_(LSeg_((Lower_Seq_(C,n)),i))_/\_(LSeg_((Lower_Seq_(C,n)),j))_=_{}
percases ( i > 0 or i = 0 ) by NAT_1:2;
suppose i > 0 ; ::_thesis: (LSeg ((Lower_Seq (C,n)),i)) /\ (LSeg ((Lower_Seq (C,n)),j)) = {}
then A50: i >= 0 + 1 by NAT_1:13;
then  i = (i -' 1) + 1 by XREAL_1:235;
then A51: LSeg ((Lower_Seq (C,n)),i) = LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),((i -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))))) by A29, SPPOL_2:10;
 (i + 1) - 1 < j - 1 by A48, XREAL_1:9;
then A52: (i - 1) + 1 < j -' 1 by XREAL_0:def_2;
 i - 1 >= 0 by A50, XREAL_1:19;
then  (i -' 1) + 1 < j -' 1 by A52, XREAL_0:def_2;
then  ((i -' 1) + 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) < (j -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by XREAL_1:6;
then A53: ((i -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 < (j -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) ;
A54: (i -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) > 0 + 1 by A28, XREAL_1:8;
now__::_thesis:_(LSeg_((Lower_Seq_(C,n)),i))_/\_(LSeg_((Lower_Seq_(C,n)),j))_=_{}
percases ( ((j -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 <= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) or ((j -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 > len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) ) ;
suppose ((j -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 <= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) ; ::_thesis: (LSeg ((Lower_Seq (C,n)),i)) /\ (LSeg ((Lower_Seq (C,n)),j)) = {}
then  (j -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) < len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by NAT_1:13;
then  LSeg ((Lower_Seq (C,n)),i) misses LSeg ((Lower_Seq (C,n)),j) by A49, A51, A53, A54, GOBOARD5:def_4;
hence  (LSeg ((Lower_Seq (C,n)),i)) /\ (LSeg ((Lower_Seq (C,n)),j)) = {} by XBOOLE_0:def_7; ::_thesis: verum
end;
suppose ((j -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 > len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) ; ::_thesis: (LSeg ((Lower_Seq (C,n)),i)) /\ (LSeg ((Lower_Seq (C,n)),j)) = {}
then  LSeg ((Lower_Seq (C,n)),j) = {} by A49, TOPREAL1:def_3;
hence  (LSeg ((Lower_Seq (C,n)),i)) /\ (LSeg ((Lower_Seq (C,n)),j)) = {} ; ::_thesis: verum
end;
end;
end;
hence  (LSeg ((Lower_Seq (C,n)),i)) /\ (LSeg ((Lower_Seq (C,n)),j)) = {} ; ::_thesis: verum
end;
suppose i = 0 ; ::_thesis: (LSeg ((Lower_Seq (C,n)),i)) /\ (LSeg ((Lower_Seq (C,n)),j)) = {}
then  LSeg ((Lower_Seq (C,n)),i) = {} by TOPREAL1:def_3;
hence  (LSeg ((Lower_Seq (C,n)),i)) /\ (LSeg ((Lower_Seq (C,n)),j)) = {} ; ::_thesis: verum
end;
end;
end;
hence  LSeg ((Lower_Seq (C,n)),i) misses LSeg ((Lower_Seq (C,n)),j) by XBOOLE_0:def_7; ::_thesis: verum
end;
end;

theorem Th10: :: JORDAN1E:10
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT holds (len (Upper_Seq (C,n))) + (len (Lower_Seq (C,n))) = (len (Cage (C,n))) + 1
proof
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT holds (len (Upper_Seq (C,n))) + (len (Lower_Seq (C,n))) = (len (Cage (C,n))) + 1
let n be Element of NAT ; ::_thesis: (len (Upper_Seq (C,n))) + (len (Lower_Seq (C,n))) = (len (Cage (C,n))) + 1
thus (len (Upper_Seq (C,n))) + (len (Lower_Seq (C,n))) = ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) + (len (Lower_Seq (C,n))) by Th8
.= ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) + (((len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1) by Th9
.= ((((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) + (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1
.= (len (Cage (C,n))) + 1 by REVROT_1:14 ; ::_thesis: verum
end;

theorem Th11: :: JORDAN1E:11
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT holds Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))) = (Upper_Seq (C,n)) ^' (Lower_Seq (C,n))
proof
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT holds Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))) = (Upper_Seq (C,n)) ^' (Lower_Seq (C,n))
let n be Element of NAT ; ::_thesis: Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))) = (Upper_Seq (C,n)) ^' (Lower_Seq (C,n))
A1: dom (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) = Seg (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by FINSEQ_1:def_3;
A2: (len ((Upper_Seq (C,n)) ^' (Lower_Seq (C,n)))) + 1 = (len (Upper_Seq (C,n))) + (len (Lower_Seq (C,n))) by GRAPH_2:13
.= (len (Cage (C,n))) + 1 by Th10
.= (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) + 1 by REVROT_1:14 ;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_(Rotate_((Cage_(C,n)),(W-min_(L~_(Cage_(C,n))))))_holds_
((Upper_Seq_(C,n))_^'_(Lower_Seq_(C,n)))_._i_=_(Rotate_((Cage_(C,n)),(W-min_(L~_(Cage_(C,n))))))_._i
let i be Nat; ::_thesis: ( i in dom (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) implies ((Upper_Seq (C,n)) ^' (Lower_Seq (C,n))) . b1 = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) . b1 )
 E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;
then A3: E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:90, SPRECT_2:43;
assume A4: i in dom (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) ; ::_thesis: ((Upper_Seq (C,n)) ^' (Lower_Seq (C,n))) . b1 = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) . b1
then A5: 1 <= i by A1, FINSEQ_1:1;
A6: i <= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A1, A4, FINSEQ_1:1;
percases ( i <= len (Upper_Seq (C,n)) or i > len (Upper_Seq (C,n)) ) ;
supposeA7: i <= len (Upper_Seq (C,n)) ; ::_thesis: ((Upper_Seq (C,n)) ^' (Lower_Seq (C,n))) . b1 = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) . b1
then  i <= (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by Th8;
then A8: i in Seg ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A5, FINSEQ_1:1;
 len ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n))))) = (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A3, FINSEQ_5:42;
then A9: i in dom ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n))))) by A8, FINSEQ_1:def_3;
 i in NAT by ORDINAL1:def_12;
hence ((Upper_Seq (C,n)) ^' (Lower_Seq (C,n))) . i = ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n))))) . i by A5, A7, GRAPH_2:14
.= ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n))))) /. i by A9, PARTFUN1:def_6
.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. i by A3, A8, FINSEQ_5:43
.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) . i by A4, PARTFUN1:def_6 ;
::_thesis: verum
end;
suppose i > len (Upper_Seq (C,n)) ; ::_thesis: ((Upper_Seq (C,n)) ^' (Lower_Seq (C,n))) . b1 = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) . b1
then  i >= (len (Upper_Seq (C,n))) + 1 by NAT_1:13;
then consider j being Nat such that
A10: i = ((len (Upper_Seq (C,n))) + 1) + j by NAT_1:10;
reconsider j = j as Element of NAT by ORDINAL1:def_12;
A11: i = (len (Upper_Seq (C,n))) + (j + 1) by A10;
then A12: i = ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) + (j + 1) by Th8;
A13: len ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n))))) = ((len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 by A3, FINSEQ_5:50;
 (j + 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) <= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A6, A11, Th8;
then  j + 1 <= (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by XREAL_1:19;
then  ( (j + 1) + 1 >= 1 & (j + 1) + 1 <= len ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n))))) ) by A13, NAT_1:11, XREAL_1:7;
then A14: (j + 1) + 1 in dom ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n))))) by FINSEQ_3:25;
 i < (len ((Upper_Seq (C,n)) ^' (Lower_Seq (C,n)))) + 1 by A2, A6, NAT_1:13;
then  i < (len (Lower_Seq (C,n))) + (len (Upper_Seq (C,n))) by GRAPH_2:13;
then  i - (len (Upper_Seq (C,n))) < len (Lower_Seq (C,n)) by XREAL_1:19;
hence ((Upper_Seq (C,n)) ^' (Lower_Seq (C,n))) . i = ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n))))) . ((j + 1) + 1) by A11, GRAPH_2:15, NAT_1:11
.= ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) :- (E-max (L~ (Cage (C,n))))) /. ((j + 1) + 1) by A14, PARTFUN1:def_6
.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. ((j + 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) by A3, A14, FINSEQ_5:52
.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) . i by A4, A12, PARTFUN1:def_6 ;
::_thesis: verum
end;
end;
end;
hence  Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))) = (Upper_Seq (C,n)) ^' (Lower_Seq (C,n)) by A2, FINSEQ_2:9; ::_thesis: verum
end;

theorem :: JORDAN1E:12
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT holds L~ (Cage (C,n)) = L~ ((Upper_Seq (C,n)) ^' (Lower_Seq (C,n)))
proof
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT holds L~ (Cage (C,n)) = L~ ((Upper_Seq (C,n)) ^' (Lower_Seq (C,n)))
let n be Element of NAT ; ::_thesis: L~ (Cage (C,n)) = L~ ((Upper_Seq (C,n)) ^' (Lower_Seq (C,n)))
 Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))) = (Upper_Seq (C,n)) ^' (Lower_Seq (C,n)) by Th11;
hence  L~ (Cage (C,n)) = L~ ((Upper_Seq (C,n)) ^' (Lower_Seq (C,n))) by REVROT_1:33; ::_thesis: verum
end;

theorem :: JORDAN1E:13
for C being non empty compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT holds L~ (Cage (C,n)) = (L~ (Upper_Seq (C,n))) \/ (L~ (Lower_Seq (C,n)))
proof
let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT holds L~ (Cage (C,n)) = (L~ (Upper_Seq (C,n))) \/ (L~ (Lower_Seq (C,n)))
let n be Element of NAT ; ::_thesis: L~ (Cage (C,n)) = (L~ (Upper_Seq (C,n))) \/ (L~ (Lower_Seq (C,n)))
 E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;
then  E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:90, SPRECT_2:43;
then  L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) = (L~ (Upper_Seq (C,n))) \/ (L~ (Lower_Seq (C,n))) by SPPOL_2:24;
hence  L~ (Cage (C,n)) = (L~ (Upper_Seq (C,n))) \/ (L~ (Lower_Seq (C,n))) by REVROT_1:33; ::_thesis: verum
end;

theorem Th14: :: JORDAN1E:14
for P being Simple_closed_curve holds W-min P <> E-min P
proof
let P be Simple_closed_curve; ::_thesis: W-min P <> E-min P
now__::_thesis:_not_W-min_P_=_E-min_P
assume  W-min P = E-min P ; ::_thesis: contradiction
then  W-bound P = E-bound P by SPPOL_2:1;
hence  contradiction by TOPREAL5:17; ::_thesis: verum
end;
hence  W-min P <> E-min P ; ::_thesis: verum
end;

theorem Th15: :: JORDAN1E:15
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT holds
( len (Upper_Seq (C,n)) >= 3 & len (Lower_Seq (C,n)) >= 3 )
proof
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT holds
( len (Upper_Seq (C,n)) >= 3 & len (Lower_Seq (C,n)) >= 3 )
let n be Element of NAT ; ::_thesis: ( len (Upper_Seq (C,n)) >= 3 & len (Lower_Seq (C,n)) >= 3 )
set pWi = W-min (L~ (Cage (C,n)));
set pWa = W-max (L~ (Cage (C,n)));
set pEi = E-min (L~ (Cage (C,n)));
set pEa = E-max (L~ (Cage (C,n)));
A1: W-min (L~ (Cage (C,n))) <> E-max (L~ (Cage (C,n))) by TOPREAL5:19;
set f = Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))));
A2: W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:43;
 E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;
then A3: E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:90, SPRECT_2:43;
then (Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by FINSEQ_5:54
.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1 by FINSEQ_6:def_1
.= W-min (L~ (Cage (C,n))) by A2, FINSEQ_6:92 ;
then A4: ( E-max (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) & W-min (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) ) by FINSEQ_6:61, REVROT_1:3;
 (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) <= (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) ;
then A5: E-max (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) by A3, FINSEQ_5:46;
 W-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:44;
then A6: W-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:90, SPRECT_2:43;
A7: (Upper_Seq (C,n)) /. 1 = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1 by A3, FINSEQ_5:44;
then A8: (Upper_Seq (C,n)) /. 1 = W-min (L~ (Cage (C,n))) by A2, FINSEQ_6:92;
then A9: W-min (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) by FINSEQ_6:42;
A10: L~ (Cage (C,n)) = L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by REVROT_1:33;
then  (W-max (L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) <= (N-min (L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A2, A7, FINSEQ_6:92, SPRECT_5:23;
then A11: (W-max (L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) < (N-max (L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A7, A8, A10, SPRECT_5:24, XXREAL_0:2;
 (N-max (L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) <= (E-max (L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A2, A7, A10, FINSEQ_6:92, SPRECT_5:25;
then A12: W-max (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) by A3, A6, A10, A11, FINSEQ_5:46, XXREAL_0:2;
 {(W-min (L~ (Cage (C,n)))),(W-max (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} c= rng (Upper_Seq (C,n))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(W-min (L~ (Cage (C,n)))),(W-max (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} or x in rng (Upper_Seq (C,n)) )
assume  x in {(W-min (L~ (Cage (C,n)))),(W-max (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} ; ::_thesis: x in rng (Upper_Seq (C,n))
hence  x in rng (Upper_Seq (C,n)) by A5, A9, A12, ENUMSET1:def_1; ::_thesis: verum
end;
then A13: card {(W-min (L~ (Cage (C,n)))),(W-max (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} c= card (rng (Upper_Seq (C,n))) by CARD_1:11;
 card (rng (Upper_Seq (C,n))) c= card (dom (Upper_Seq (C,n))) by CARD_2:61;
then A14: card (rng (Upper_Seq (C,n))) c= len (Upper_Seq (C,n)) by CARD_1:62;
 ( W-min (L~ (Cage (C,n))) <> W-max (L~ (Cage (C,n))) & W-max (L~ (Cage (C,n))) <> E-max (L~ (Cage (C,n))) ) by JORDAN1B:5, SPRECT_2:58;
then  card {(W-min (L~ (Cage (C,n)))),(W-max (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} = 3 by A1, CARD_2:58;
then  3 c= len (Upper_Seq (C,n)) by A13, A14, XBOOLE_1:1;
hence  len (Upper_Seq (C,n)) >= 3 by NAT_1:39; ::_thesis: len (Lower_Seq (C,n)) >= 3
A15: W-min (L~ (Cage (C,n))) <> E-max (L~ (Cage (C,n))) by TOPREAL5:19;
 E-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:45;
then A16: E-min (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:90, SPRECT_2:43;
 (E-min (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) > (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A2, A7, A10, FINSEQ_6:92, SPRECT_5:26;
then A17: E-min (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) by A3, A16, FINSEQ_6:62;
 {(W-min (L~ (Cage (C,n)))),(E-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} c= rng (Lower_Seq (C,n))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(W-min (L~ (Cage (C,n)))),(E-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} or x in rng (Lower_Seq (C,n)) )
assume  x in {(W-min (L~ (Cage (C,n)))),(E-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} ; ::_thesis: x in rng (Lower_Seq (C,n))
hence  x in rng (Lower_Seq (C,n)) by A4, A17, ENUMSET1:def_1; ::_thesis: verum
end;
then A18: card {(W-min (L~ (Cage (C,n)))),(E-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} c= card (rng (Lower_Seq (C,n))) by CARD_1:11;
 card (rng (Lower_Seq (C,n))) c= card (dom (Lower_Seq (C,n))) by CARD_2:61;
then A19: card (rng (Lower_Seq (C,n))) c= len (Lower_Seq (C,n)) by CARD_1:62;
 ( W-min (L~ (Cage (C,n))) <> E-min (L~ (Cage (C,n))) & E-min (L~ (Cage (C,n))) <> E-max (L~ (Cage (C,n))) ) by Th14, SPRECT_2:54;
then  card {(W-min (L~ (Cage (C,n)))),(E-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} = 3 by A15, CARD_2:58;
then  3 c= len (Lower_Seq (C,n)) by A18, A19, XBOOLE_1:1;
hence  len (Lower_Seq (C,n)) >= 3 by NAT_1:39; ::_thesis: verum
end;

registration
let C be compact non horizontal non vertical Subset of (TOP-REAL 2);
let n be Element of NAT ;
cluster Upper_Seq (C,n) ->  being_S-Seq ;
coherence
 Upper_Seq (C,n) is being_S-Seq
proof
 len (Upper_Seq (C,n)) >= 3 by Th15;
then  len (Upper_Seq (C,n)) >= 2 by XXREAL_0:2;
hence  Upper_Seq (C,n) is being_S-Seq by TOPREAL1:def_8; ::_thesis: verum
end;
cluster Lower_Seq (C,n) ->  being_S-Seq ;
coherence
 Lower_Seq (C,n) is being_S-Seq
proof
 len (Lower_Seq (C,n)) >= 3 by Th15;
then  len (Lower_Seq (C,n)) >= 2 by XXREAL_0:2;
hence  Lower_Seq (C,n) is being_S-Seq by TOPREAL1:def_8; ::_thesis: verum
end;
end;

theorem :: JORDAN1E:16
for C being compact non horizontal non vertical Subset of (TOP-REAL 2)
for n being Element of NAT holds (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) = {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))}
proof
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for n being Element of NAT holds (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) = {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))}
let n be Element of NAT ; ::_thesis: (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) = {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))}
 E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;
then A1: E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:90, SPRECT_2:43;
A2: len (Upper_Seq (C,n)) >= 3 by Th15;
then A3: rng (Upper_Seq (C,n)) c= L~ (Upper_Seq (C,n)) by SPPOL_2:18, XXREAL_0:2;
A4: W-min (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:43;
thus  (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) c= {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} :: according to XBOOLE_0:def_10 ::_thesis: {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} c= (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n)))
proof
set pW = W-min (L~ (Cage (C,n)));
set pE = E-max (L~ (Cage (C,n)));
set f = Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))));
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) or x in {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} )
assume A5: x in (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) ; ::_thesis: x in {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))}
then reconsider x1 = x as Point of (TOP-REAL 2) ;
assume A6: not x in {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} ; ::_thesis: contradiction
 x in L~ (Upper_Seq (C,n)) by A5, XBOOLE_0:def_4;
then consider i1 being Element of NAT  such that
A7: 1 <= i1 and
A8: i1 + 1 <= len (Upper_Seq (C,n)) and
A9: x1 in LSeg ((Upper_Seq (C,n)),i1) by SPPOL_2:13;
A10: LSeg ((Upper_Seq (C,n)),i1) = LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),i1) by A8, SPPOL_2:9;
 x in L~ (Lower_Seq (C,n)) by A5, XBOOLE_0:def_4;
then consider i2 being Element of NAT  such that
A11: 1 <= i2 and
A12: i2 + 1 <= len (Lower_Seq (C,n)) and
A13: x1 in LSeg ((Lower_Seq (C,n)),i2) by SPPOL_2:13;
set i3 = i2 -' 1;
A14: (i2 -' 1) + 1 = i2 by A11, XREAL_1:235;
then A15: 1 + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) <= ((i2 -' 1) + 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A11, XREAL_1:7;
A16: len (Lower_Seq (C,n)) = ((len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 by Th9;
then  i2 < ((len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 by A12, NAT_1:13;
then  i2 - 1 < (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by XREAL_1:19;
then A17: (i2 - 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) < len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by XREAL_1:20;
 i2 - 1 >= 1 - 1 by A11, XREAL_1:9;
then A18: (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) < len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A17, XREAL_0:def_2;
A19: (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) >= 0 by NAT_1:2;
A20: LSeg ((Lower_Seq (C,n)),i2) = LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))))) by A1, A14, SPPOL_2:10;
A21: len (Upper_Seq (C,n)) = (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by Th8;
then  i1 + 1 < ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) + 1 by A8, NAT_1:13;
then  i1 + 1 < ((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 by A15, XXREAL_0:2;
then A22: i1 + 1 <= (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by NAT_1:13;
A23: (((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) -' 1) + 1 = (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A1, FINSEQ_4:21, XREAL_1:235;
 (i2 -' 1) + 1 < ((len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 by A12, A14, A16, NAT_1:13;
then  i2 -' 1 < (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by XREAL_1:7;
then A24: (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) < len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by XREAL_1:20;
then A25: ((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 <= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by NAT_1:13;
now__::_thesis:_contradiction
percases ( ( i1 + 1 < (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) & i1 > 1 ) or i1 = 1 or i1 + 1 = (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) ) by A7, A22, XXREAL_0:1;
suppose ( i1 + 1 < (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) & i1 > 1 ) ; ::_thesis: contradiction
then  LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),i1) misses LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))))) by A24, GOBOARD5:def_4;
then  (LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),i1)) /\ (LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))))) = {} by XBOOLE_0:def_7;
hence  contradiction by A9, A13, A10, A20, XBOOLE_0:def_4; ::_thesis: verum
end;
supposeA26: i1 = 1 ; ::_thesis: contradiction
 (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) >= 0 + 3 by A2, A21, XREAL_1:7;
then A27: i1 + 1 < (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A26, XXREAL_0:2;
now__::_thesis:_contradiction
percases ( ((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 < len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) or ((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 = len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) ) by A25, XXREAL_0:1;
suppose ((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 < len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) ; ::_thesis: contradiction
then  LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),i1) misses LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))))) by A27, GOBOARD5:def_4;
then  (LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),i1)) /\ (LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))))) = {} by XBOOLE_0:def_7;
hence  contradiction by A9, A13, A10, A20, XBOOLE_0:def_4; ::_thesis: verum
end;
suppose ((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))) + 1 = len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) ; ::_thesis: contradiction
then  (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) = (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) - 1 ;
then  (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) = (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) -' 1 by A19, XREAL_0:def_2;
then  (LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),i1)) /\ (LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))))) = {((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1)} by A26, GOBOARD7:34, REVROT_1:30;
then  x1 in {((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1)} by A9, A13, A10, A20, XBOOLE_0:def_4;
then x1 = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1 by TARSKI:def_1
.= W-min (L~ (Cage (C,n))) by A4, FINSEQ_6:92 ;
hence  contradiction by A6, TARSKI:def_2; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
supposeA28: i1 + 1 = (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) ; ::_thesis: contradiction
 (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) >= (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by NAT_1:11;
then  (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) < len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A18, XXREAL_0:2;
then  ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) + 1 <= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by NAT_1:13;
then A29: (((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) -' 1) + (1 + 1) <= len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by A23;
 0 + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) <= (i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by XREAL_1:7;
then  (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) = i1 + 1 by A8, A21, A28, XXREAL_0:1;
then  (LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),i1)) /\ (LSeg ((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))),((i2 -' 1) + ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))))))) = {((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))))} by A7, A23, A28, A29, TOPREAL1:def_6;
then  x1 in {((Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))))} by A9, A13, A10, A20, XBOOLE_0:def_4;
then x1 = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. ((E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by TARSKI:def_1
.= E-max (L~ (Cage (C,n))) by A1, FINSEQ_5:38 ;
hence  contradiction by A6, TARSKI:def_2; ::_thesis: verum
end;
end;
end;
hence  contradiction ; ::_thesis: verum
end;
(Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. (len (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))) by A1, FINSEQ_5:54
.= (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1 by FINSEQ_6:def_1
.= W-min (L~ (Cage (C,n))) by A4, FINSEQ_6:92 ;
then A30: W-min (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) by REVROT_1:3;
 (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) <= (E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) ;
then A31: ( E-max (L~ (Cage (C,n))) in rng (Lower_Seq (C,n)) & E-max (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) ) by A1, FINSEQ_5:46, FINSEQ_6:61;
 len (Lower_Seq (C,n)) >= 3 by Th15;
then A32: rng (Lower_Seq (C,n)) c= L~ (Lower_Seq (C,n)) by SPPOL_2:18, XXREAL_0:2;
(Upper_Seq (C,n)) /. 1 = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1 by A1, FINSEQ_5:44
.= W-min (L~ (Cage (C,n))) by A4, FINSEQ_6:92 ;
then A33: W-min (L~ (Cage (C,n))) in rng (Upper_Seq (C,n)) by FINSEQ_6:42;
thus  {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} c= (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} or x in (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) )
assume A34: x in {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} ; ::_thesis: x in (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n)))
percases ( x = W-min (L~ (Cage (C,n))) or x = E-max (L~ (Cage (C,n))) ) by A34, TARSKI:def_2;
suppose x = W-min (L~ (Cage (C,n))) ; ::_thesis: x in (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n)))
hence  x in (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) by A32, A3, A33, A30, XBOOLE_0:def_4; ::_thesis: verum
end;
suppose x = E-max (L~ (Cage (C,n))) ; ::_thesis: x in (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n)))
hence  x in (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n))) by A32, A3, A31, XBOOLE_0:def_4; ::_thesis: verum
end;
end;
end;
end;

theorem :: JORDAN1E:17
for n being Element of NAT
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds Upper_Seq (C,n) is_in_the_area_of Cage (C,n)
proof
let n be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds Upper_Seq (C,n) is_in_the_area_of Cage (C,n)
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: Upper_Seq (C,n) is_in_the_area_of Cage (C,n)
 E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;
then  E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:90, SPRECT_2:43;
hence  Upper_Seq (C,n) is_in_the_area_of Cage (C,n) by Th1, JORDAN1B:10; ::_thesis: verum
end;

theorem :: JORDAN1E:18
for n being Element of NAT
for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds Lower_Seq (C,n) is_in_the_area_of Cage (C,n)
proof
let n be Element of NAT ; ::_thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) holds Lower_Seq (C,n) is_in_the_area_of Cage (C,n)
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: Lower_Seq (C,n) is_in_the_area_of Cage (C,n)
 E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) by SPRECT_2:46;
then  E-max (L~ (Cage (C,n))) in rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) by FINSEQ_6:90, SPRECT_2:43;
hence  Lower_Seq (C,n) is_in_the_area_of Cage (C,n) by Th2, JORDAN1B:10; ::_thesis: verum
end;

theorem :: JORDAN1E:19
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds ((Cage (C,n)) /. 2) `2 = N-bound (L~ (Cage (C,n)))
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2) holds ((Cage (C,n)) /. 2) `2 = N-bound (L~ (Cage (C,n)))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: ((Cage (C,n)) /. 2) `2 = N-bound (L~ (Cage (C,n)))
 (Cage (C,n)) /. 1 = N-min (L~ (Cage (C,n))) by JORDAN9:32;
then  (Cage (C,n)) /. 2 in N-most (L~ (Cage (C,n))) by SPRECT_2:30;
then  ((Cage (C,n)) /. 2) `2 = (N-min (L~ (Cage (C,n)))) `2 by PSCOMP_1:39;
hence  ((Cage (C,n)) /. 2) `2 = N-bound (L~ (Cage (C,n))) by EUCLID:52; ::_thesis: verum
end;

theorem :: JORDAN1E:20
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for k being Element of NAT st 1 <= k & k + 1 <= len (Cage (C,n)) & (Cage (C,n)) /. k = E-max (L~ (Cage (C,n))) holds
((Cage (C,n)) /. (k + 1)) `1 = E-bound (L~ (Cage (C,n)))
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for k being Element of NAT st 1 <= k & k + 1 <= len (Cage (C,n)) & (Cage (C,n)) /. k = E-max (L~ (Cage (C,n))) holds
((Cage (C,n)) /. (k + 1)) `1 = E-bound (L~ (Cage (C,n)))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for k being Element of NAT st 1 <= k & k + 1 <= len (Cage (C,n)) & (Cage (C,n)) /. k = E-max (L~ (Cage (C,n))) holds
((Cage (C,n)) /. (k + 1)) `1 = E-bound (L~ (Cage (C,n)))
A1: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
A2: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
A3: (Cage (C,n)) /. 1 = N-min (L~ (Cage (C,n))) by JORDAN9:32;
then  1 < (N-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by SPRECT_2:69;
then A4: (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1 by A3, SPRECT_2:70, XXREAL_0:2;
let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len (Cage (C,n)) & (Cage (C,n)) /. k = E-max (L~ (Cage (C,n))) implies ((Cage (C,n)) /. (k + 1)) `1 = E-bound (L~ (Cage (C,n))) )
assume that
A5: 1 <= k and
A6: k + 1 <= len (Cage (C,n)) and
A7: (Cage (C,n)) /. k = E-max (L~ (Cage (C,n))) ; ::_thesis: ((Cage (C,n)) /. (k + 1)) `1 = E-bound (L~ (Cage (C,n)))
A8: k < len (Cage (C,n)) by A6, NAT_1:13;
then A9: k in dom (Cage (C,n)) by A5, FINSEQ_3:25;
then reconsider k9 = k - 1 as Element of NAT by FINSEQ_3:26;
 (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) <= k by A7, A9, FINSEQ_5:39;
then A10: k > 1 by A4, XXREAL_0:2;
then consider i1, j1, i2, j2 being Element of NAT  such that
A11: [i1,j1] in Indices (Gauge (C,n)) and
A12: (Cage (C,n)) /. k = (Gauge (C,n)) * (i1,j1) and
A13: [i2,j2] in Indices (Gauge (C,n)) and
A14: (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * (i2,j2) and
A15: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A1, A6, JORDAN8:3;
A16: 1 <= i1 by A11, MATRIX_1:38;
A17: k9 + 1 < len (Cage (C,n)) by A6, NAT_1:13;
A18: 1 <= j1 by A11, MATRIX_1:38;
A19: j2 <= width (Gauge (C,n)) by A13, MATRIX_1:38;
A20: i2 <= len (Gauge (C,n)) by A13, MATRIX_1:38;
A21: j1 <= width (Gauge (C,n)) by A11, MATRIX_1:38;
((Gauge (C,n)) * (i1,j1)) `1 = E-bound (L~ (Cage (C,n))) by A7, A12, EUCLID:52
.= ((Gauge (C,n)) * ((len (Gauge (C,n))),j1)) `1 by A18, A21, A2, JORDAN1A:71 ;
then A22: i1 >= len (Gauge (C,n)) by A16, A18, A21, GOBOARD5:3;
 k >= 1 + 1 by A10, NAT_1:13;
then A23: k9 >= (1 + 1) - 1 by XREAL_1:9;
then consider i3, j3, i4, j4 being Element of NAT  such that
A24: [i3,j3] in Indices (Gauge (C,n)) and
A25: (Cage (C,n)) /. k9 = (Gauge (C,n)) * (i3,j3) and
A26: [i4,j4] in Indices (Gauge (C,n)) and
A27: (Cage (C,n)) /. (k9 + 1) = (Gauge (C,n)) * (i4,j4) and
A28: ( ( i3 = i4 & j3 + 1 = j4 ) or ( i3 + 1 = i4 & j3 = j4 ) or ( i3 = i4 + 1 & j3 = j4 ) or ( i3 = i4 & j3 = j4 + 1 ) ) by A1, A8, JORDAN8:3;
A29: i1 = i4 by A11, A12, A26, A27, GOBOARD1:5;
A30: j1 = j4 by A11, A12, A26, A27, GOBOARD1:5;
A31: 1 <= j3 by A24, MATRIX_1:38;
A32: j3 <= width (Gauge (C,n)) by A24, MATRIX_1:38;
A33: i1 <= len (Gauge (C,n)) by A11, MATRIX_1:38;
then A34: i1 = len (Gauge (C,n)) by A22, XXREAL_0:1;
A35: j3 = j4
proof
assume A36: j3 <> j4 ; ::_thesis: contradiction
percases ( ( i3 = i4 & j3 + 1 = j4 ) or ( i3 = i4 & j3 = j4 + 1 ) ) by A28, A36;
suppose ( i3 = i4 & j3 + 1 = j4 ) ; ::_thesis: contradiction
hence  contradiction by A8, A22, A23, A24, A25, A26, A27, A29, JORDAN10:1; ::_thesis: verum
end;
supposeA37: ( i3 = i4 & j3 = j4 + 1 ) ; ::_thesis: contradiction
 k9 < len (Cage (C,n)) by A17, NAT_1:13;
then  (Gauge (C,n)) * (i3,j3) in E-most (L~ (Cage (C,n))) by A34, A23, A25, A29, A31, A32, A37, JORDAN1A:61;
then A38: ((Gauge (C,n)) * (i4,(j4 + 1))) `2 <= ((Gauge (C,n)) * (i4,j4)) `2 by A7, A27, A37, PSCOMP_1:47;
 j4 < j4 + 1 by NAT_1:13;
hence  contradiction by A16, A33, A18, A29, A30, A32, A37, A38, GOBOARD5:4; ::_thesis: verum
end;
end;
end;
A39: ( 1 <= i2 & 1 <= j2 ) by A13, MATRIX_1:38;
A40: k9 + 1 = k ;
A41: i3 <= len (Gauge (C,n)) by A24, MATRIX_1:38;
 i1 = i2
proof
assume A42: i1 <> i2 ; ::_thesis: contradiction
percases ( ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) ) by A15, A42;
suppose ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: contradiction
hence  contradiction by A20, A22, NAT_1:13; ::_thesis: verum
end;
supposeA43: ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: contradiction
 k9 + (1 + 1) <= len (Cage (C,n)) by A6;
then A44: (LSeg ((Cage (C,n)),k9)) /\ (LSeg ((Cage (C,n)),k)) = {((Cage (C,n)) /. k)} by A23, A40, TOPREAL1:def_6;
 ( (Cage (C,n)) /. k9 in LSeg ((Cage (C,n)),k9) & (Cage (C,n)) /. (k + 1) in LSeg ((Cage (C,n)),k) ) by A5, A6, A8, A23, A40, TOPREAL1:21;
then  (Cage (C,n)) /. (k + 1) in {((Cage (C,n)) /. k)} by A14, A22, A25, A28, A29, A30, A41, A35, A43, A44, NAT_1:13, XBOOLE_0:def_4;
then  (Cage (C,n)) /. (k + 1) = (Cage (C,n)) /. k by TARSKI:def_1;
hence  contradiction by A11, A12, A13, A14, A42, GOBOARD1:5; ::_thesis: verum
end;
end;
end;
then ((Gauge (C,n)) * (i1,j1)) `1 = ((Gauge (C,n)) * (i2,1)) `1 by A16, A33, A18, A21, GOBOARD5:2
.= ((Gauge (C,n)) * (i2,j2)) `1 by A20, A39, A19, GOBOARD5:2 ;
hence  ((Cage (C,n)) /. (k + 1)) `1 = E-bound (L~ (Cage (C,n))) by A7, A12, A14, EUCLID:52; ::_thesis: verum
end;

theorem :: JORDAN1E:21
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for k being Element of NAT st 1 <= k & k + 1 <= len (Cage (C,n)) & (Cage (C,n)) /. k = S-max (L~ (Cage (C,n))) holds
((Cage (C,n)) /. (k + 1)) `2 = S-bound (L~ (Cage (C,n)))
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for k being Element of NAT st 1 <= k & k + 1 <= len (Cage (C,n)) & (Cage (C,n)) /. k = S-max (L~ (Cage (C,n))) holds
((Cage (C,n)) /. (k + 1)) `2 = S-bound (L~ (Cage (C,n)))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for k being Element of NAT st 1 <= k & k + 1 <= len (Cage (C,n)) & (Cage (C,n)) /. k = S-max (L~ (Cage (C,n))) holds
((Cage (C,n)) /. (k + 1)) `2 = S-bound (L~ (Cage (C,n)))
A1: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
A2: (Cage (C,n)) /. 1 = N-min (L~ (Cage (C,n))) by JORDAN9:32;
then  1 < (N-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by SPRECT_2:69;
then  1 < (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by A2, SPRECT_2:70, XXREAL_0:2;
then  1 < (E-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A2, SPRECT_2:71, XXREAL_0:2;
then A3: (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1 by A2, SPRECT_2:72, XXREAL_0:2;
let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len (Cage (C,n)) & (Cage (C,n)) /. k = S-max (L~ (Cage (C,n))) implies ((Cage (C,n)) /. (k + 1)) `2 = S-bound (L~ (Cage (C,n))) )
assume that
A4: 1 <= k and
A5: k + 1 <= len (Cage (C,n)) and
A6: (Cage (C,n)) /. k = S-max (L~ (Cage (C,n))) ; ::_thesis: ((Cage (C,n)) /. (k + 1)) `2 = S-bound (L~ (Cage (C,n)))
A7: k < len (Cage (C,n)) by A5, NAT_1:13;
then A8: k in dom (Cage (C,n)) by A4, FINSEQ_3:25;
then reconsider k9 = k - 1 as Element of NAT by FINSEQ_3:26;
 (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) <= k by A6, A8, FINSEQ_5:39;
then A9: k > 1 by A3, XXREAL_0:2;
then consider i1, j1, i2, j2 being Element of NAT  such that
A10: [i1,j1] in Indices (Gauge (C,n)) and
A11: (Cage (C,n)) /. k = (Gauge (C,n)) * (i1,j1) and
A12: [i2,j2] in Indices (Gauge (C,n)) and
A13: (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * (i2,j2) and
A14: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A1, A5, JORDAN8:3;
A15: 1 <= i1 by A10, MATRIX_1:38;
A16: j2 <= width (Gauge (C,n)) by A12, MATRIX_1:38;
A17: 1 <= j2 by A12, MATRIX_1:38;
A18: j1 <= width (Gauge (C,n)) by A10, MATRIX_1:38;
A19: k9 + 1 < len (Cage (C,n)) by A5, NAT_1:13;
A20: i1 <= len (Gauge (C,n)) by A10, MATRIX_1:38;
((Gauge (C,n)) * (i1,j1)) `2 = S-bound (L~ (Cage (C,n))) by A6, A11, EUCLID:52
.= ((Gauge (C,n)) * (i1,1)) `2 by A15, A20, JORDAN1A:72 ;
then A21: j1 <= 1 by A15, A20, A18, GOBOARD5:4;
 k >= 1 + 1 by A9, NAT_1:13;
then A22: k9 >= (1 + 1) - 1 by XREAL_1:9;
then consider i3, j3, i4, j4 being Element of NAT  such that
A23: [i3,j3] in Indices (Gauge (C,n)) and
A24: (Cage (C,n)) /. k9 = (Gauge (C,n)) * (i3,j3) and
A25: [i4,j4] in Indices (Gauge (C,n)) and
A26: (Cage (C,n)) /. (k9 + 1) = (Gauge (C,n)) * (i4,j4) and
A27: ( ( i3 = i4 & j3 + 1 = j4 ) or ( i3 + 1 = i4 & j3 = j4 ) or ( i3 = i4 + 1 & j3 = j4 ) or ( i3 = i4 & j3 = j4 + 1 ) ) by A1, A7, JORDAN8:3;
A28: i1 = i4 by A10, A11, A25, A26, GOBOARD1:5;
A29: j1 = j4 by A10, A11, A25, A26, GOBOARD1:5;
A30: 1 <= i3 by A23, MATRIX_1:38;
A31: i3 <= len (Gauge (C,n)) by A23, MATRIX_1:38;
A32: 1 <= j1 by A10, MATRIX_1:38;
then A33: j1 = 1 by A21, XXREAL_0:1;
A34: i3 = i4
proof
assume A35: i3 <> i4 ; ::_thesis: contradiction
percases ( ( j3 = j4 & i3 + 1 = i4 ) or ( j3 = j4 & i3 = i4 + 1 ) ) by A27, A35;
suppose ( j3 = j4 & i3 + 1 = i4 ) ; ::_thesis: contradiction
hence  contradiction by A7, A21, A22, A23, A24, A25, A26, A29, JORDAN10:3; ::_thesis: verum
end;
supposeA36: ( j3 = j4 & i3 = i4 + 1 ) ; ::_thesis: contradiction
 k9 < len (Cage (C,n)) by A19, NAT_1:13;
then  (Gauge (C,n)) * (i3,j3) in S-most (L~ (Cage (C,n))) by A33, A22, A24, A29, A30, A31, A36, JORDAN1A:60;
then A37: ((Gauge (C,n)) * ((i4 + 1),j4)) `1 <= ((Gauge (C,n)) * (i4,j4)) `1 by A6, A26, A36, PSCOMP_1:55;
 i4 < i4 + 1 by NAT_1:13;
hence  contradiction by A15, A32, A18, A28, A29, A31, A36, A37, GOBOARD5:3; ::_thesis: verum
end;
end;
end;
A38: ( 1 <= i2 & i2 <= len (Gauge (C,n)) ) by A12, MATRIX_1:38;
A39: k9 + 1 = k ;
A40: 1 <= j3 by A23, MATRIX_1:38;
 j1 = j2
proof
assume A41: j1 <> j2 ; ::_thesis: contradiction
percases ( ( j1 = j2 + 1 & i1 = i2 ) or ( j1 + 1 = j2 & i1 = i2 ) ) by A14, A41;
suppose ( j1 = j2 + 1 & i1 = i2 ) ; ::_thesis: contradiction
hence  contradiction by A17, A21, NAT_1:13; ::_thesis: verum
end;
supposeA42: ( j1 + 1 = j2 & i1 = i2 ) ; ::_thesis: contradiction
 k9 + (1 + 1) <= len (Cage (C,n)) by A5;
then A43: (LSeg ((Cage (C,n)),k9)) /\ (LSeg ((Cage (C,n)),k)) = {((Cage (C,n)) /. k)} by A22, A39, TOPREAL1:def_6;
 ( (Cage (C,n)) /. k9 in LSeg ((Cage (C,n)),k9) & (Cage (C,n)) /. (k + 1) in LSeg ((Cage (C,n)),k) ) by A4, A5, A7, A22, A39, TOPREAL1:21;
then  (Cage (C,n)) /. (k + 1) in {((Cage (C,n)) /. k)} by A13, A21, A24, A27, A28, A29, A40, A34, A42, A43, NAT_1:13, XBOOLE_0:def_4;
then  (Cage (C,n)) /. (k + 1) = (Cage (C,n)) /. k by TARSKI:def_1;
hence  contradiction by A10, A11, A12, A13, A41, GOBOARD1:5; ::_thesis: verum
end;
end;
end;
then ((Gauge (C,n)) * (i1,j1)) `2 = ((Gauge (C,n)) * (1,j2)) `2 by A15, A20, A32, A18, GOBOARD5:1
.= ((Gauge (C,n)) * (i2,j2)) `2 by A38, A17, A16, GOBOARD5:1 ;
hence  ((Cage (C,n)) /. (k + 1)) `2 = S-bound (L~ (Cage (C,n))) by A6, A11, A13, EUCLID:52; ::_thesis: verum
end;

theorem :: JORDAN1E:22
for n being Element of NAT
for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for k being Element of NAT st 1 <= k & k + 1 <= len (Cage (C,n)) & (Cage (C,n)) /. k = W-min (L~ (Cage (C,n))) holds
((Cage (C,n)) /. (k + 1)) `1 = W-bound (L~ (Cage (C,n)))
proof
let n be Element of NAT ; ::_thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for k being Element of NAT st 1 <= k & k + 1 <= len (Cage (C,n)) & (Cage (C,n)) /. k = W-min (L~ (Cage (C,n))) holds
((Cage (C,n)) /. (k + 1)) `1 = W-bound (L~ (Cage (C,n)))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); ::_thesis: for k being Element of NAT st 1 <= k & k + 1 <= len (Cage (C,n)) & (Cage (C,n)) /. k = W-min (L~ (Cage (C,n))) holds
((Cage (C,n)) /. (k + 1)) `1 = W-bound (L~ (Cage (C,n)))
A1: Cage (C,n) is_sequence_on Gauge (C,n) by JORDAN9:def_1;
A2: (Cage (C,n)) /. 1 = N-min (L~ (Cage (C,n))) by JORDAN9:32;
then  1 < (N-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by SPRECT_2:69;
then  1 < (E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by A2, SPRECT_2:70, XXREAL_0:2;
then  1 < (E-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A2, SPRECT_2:71, XXREAL_0:2;
then  1 < (S-max (L~ (Cage (C,n)))) .. (Cage (C,n)) by A2, SPRECT_2:72, XXREAL_0:2;
then  1 < (S-min (L~ (Cage (C,n)))) .. (Cage (C,n)) by A2, SPRECT_2:73, XXREAL_0:2;
then A3: (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) > 1 by A2, SPRECT_2:74, XXREAL_0:2;
let k be Element of NAT ; ::_thesis: ( 1 <= k & k + 1 <= len (Cage (C,n)) & (Cage (C,n)) /. k = W-min (L~ (Cage (C,n))) implies ((Cage (C,n)) /. (k + 1)) `1 = W-bound (L~ (Cage (C,n))) )
assume that
A4: 1 <= k and
A5: k + 1 <= len (Cage (C,n)) and
A6: (Cage (C,n)) /. k = W-min (L~ (Cage (C,n))) ; ::_thesis: ((Cage (C,n)) /. (k + 1)) `1 = W-bound (L~ (Cage (C,n)))
A7: k < len (Cage (C,n)) by A5, NAT_1:13;
then A8: k in dom (Cage (C,n)) by A4, FINSEQ_3:25;
then reconsider k9 = k - 1 as Element of NAT by FINSEQ_3:26;
 (W-min (L~ (Cage (C,n)))) .. (Cage (C,n)) <= k by A6, A8, FINSEQ_5:39;
then A9: k > 1 by A3, XXREAL_0:2;
then consider i1, j1, i2, j2 being Element of NAT  such that
A10: [i1,j1] in Indices (Gauge (C,n)) and
A11: (Cage (C,n)) /. k = (Gauge (C,n)) * (i1,j1) and
A12: [i2,j2] in Indices (Gauge (C,n)) and
A13: (Cage (C,n)) /. (k + 1) = (Gauge (C,n)) * (i2,j2) and
A14: ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A1, A5, JORDAN8:3;
A15: i1 <= len (Gauge (C,n)) by A10, MATRIX_1:38;
A16: j2 <= width (Gauge (C,n)) by A12, MATRIX_1:38;
A17: 1 <= i2 by A12, MATRIX_1:38;
A18: j1 <= width (Gauge (C,n)) by A10, MATRIX_1:38;
A19: len (Gauge (C,n)) = width (Gauge (C,n)) by JORDAN8:def_1;
A20: ( i2 <= len (Gauge (C,n)) & 1 <= j2 ) by A12, MATRIX_1:38;
A21: k9 + 1 = k ;
A22: k9 + 1 < len (Cage (C,n)) by A5, NAT_1:13;
A23: 1 <= j1 by A10, MATRIX_1:38;
((Gauge (C,n)) * (i1,j1)) `1 = W-bound (L~ (Cage (C,n))) by A6, A11, EUCLID:52
.= ((Gauge (C,n)) * (1,j1)) `1 by A23, A18, A19, JORDAN1A:73 ;
then A24: i1 <= 1 by A15, A23, A18, GOBOARD5:3;
 k >= 1 + 1 by A9, NAT_1:13;
then A25: k9 >= (1 + 1) - 1 by XREAL_1:9;
then consider i3, j3, i4, j4 being Element of NAT  such that
A26: [i3,j3] in Indices (Gauge (C,n)) and
A27: (Cage (C,n)) /. k9 = (Gauge (C,n)) * (i3,j3) and
A28: [i4,j4] in Indices (Gauge (C,n)) and
A29: (Cage (C,n)) /. (k9 + 1) = (Gauge (C,n)) * (i4,j4) and
A30: ( ( i3 = i4 & j3 + 1 = j4 ) or ( i3 + 1 = i4 & j3 = j4 ) or ( i3 = i4 + 1 & j3 = j4 ) or ( i3 = i4 & j3 = j4 + 1 ) ) by A1, A7, JORDAN8:3;
A31: i1 = i4 by A10, A11, A28, A29, GOBOARD1:5;
A32: j1 = j4 by A10, A11, A28, A29, GOBOARD1:5;
A33: j3 <= width (Gauge (C,n)) by A26, MATRIX_1:38;
A34: 1 <= j3 by A26, MATRIX_1:38;
A35: 1 <= i1 by A10, MATRIX_1:38;
then A36: i1 = 1 by A24, XXREAL_0:1;
A37: j3 = j4
proof
assume A38: j3 <> j4 ; ::_thesis: contradiction
percases ( ( i3 = i4 & j3 = j4 + 1 ) or ( i3 = i4 & j3 + 1 = j4 ) ) by A30, A38;
suppose ( i3 = i4 & j3 = j4 + 1 ) ; ::_thesis: contradiction
hence  contradiction by A7, A24, A25, A26, A27, A28, A29, A31, JORDAN10:2; ::_thesis: verum
end;
supposeA39: ( i3 = i4 & j3 + 1 = j4 ) ; ::_thesis: contradiction
 k9 < len (Cage (C,n)) by A22, NAT_1:13;
then  (Gauge (C,n)) * (i3,j3) in W-most (L~ (Cage (C,n))) by A36, A25, A27, A31, A34, A33, A39, JORDAN1A:59;
then A40: ((Gauge (C,n)) * (i3,(j3 + 1))) `2 <= ((Gauge (C,n)) * (i3,j3)) `2 by A6, A29, A39, PSCOMP_1:31;
 j3 < j3 + 1 by NAT_1:13;
hence  contradiction by A35, A15, A18, A31, A32, A34, A39, A40, GOBOARD5:4; ::_thesis: verum
end;
end;
end;
A41: 1 <= i3 by A26, MATRIX_1:38;
 i1 = i2
proof
assume A42: i1 <> i2 ; ::_thesis: contradiction
percases ( ( i1 = i2 + 1 & j1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) ) by A14, A42;
suppose ( i1 = i2 + 1 & j1 = j2 ) ; ::_thesis: contradiction
hence  contradiction by A17, A24, NAT_1:13; ::_thesis: verum
end;
supposeA43: ( i1 + 1 = i2 & j1 = j2 ) ; ::_thesis: contradiction
 k9 + (1 + 1) <= len (Cage (C,n)) by A5;
then A44: (LSeg ((Cage (C,n)),k9)) /\ (LSeg ((Cage (C,n)),k)) = {((Cage (C,n)) /. k)} by A25, A21, TOPREAL1:def_6;
 ( (Cage (C,n)) /. k9 in LSeg ((Cage (C,n)),k9) & (Cage (C,n)) /. (k + 1) in LSeg ((Cage (C,n)),k) ) by A4, A5, A7, A25, A21, TOPREAL1:21;
then  (Cage (C,n)) /. (k + 1) in {((Cage (C,n)) /. k)} by A13, A24, A27, A30, A31, A32, A41, A37, A43, A44, NAT_1:13, XBOOLE_0:def_4;
then  (Cage (C,n)) /. (k + 1) = (Cage (C,n)) /. k by TARSKI:def_1;
hence  contradiction by A10, A11, A12, A13, A42, GOBOARD1:5; ::_thesis: verum
end;
end;
end;
then ((Gauge (C,n)) * (i1,j1)) `1 = ((Gauge (C,n)) * (i2,1)) `1 by A35, A15, A23, A18, GOBOARD5:2
.= ((Gauge (C,n)) * (i2,j2)) `1 by A17, A20, A16, GOBOARD5:2 ;
hence  ((Cage (C,n)) /. (k + 1)) `1 = W-bound (L~ (Cage (C,n))) by A6, A11, A13, EUCLID:52; ::_thesis: verum
end;