let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n being Element of NAT holds Lower_Seq C,n is_sequence_on Gauge C,n
let n be Element of NAT ; :: thesis: Lower_Seq C,n is_sequence_on Gauge C,n
consider j being Element of NAT such that
A1: ( 1 <= j & j <= width (Gauge C,n) ) and
A2: E-max (L~ (Cage C,n)) = (Gauge C,n) * (len (Gauge C,n)),j by JORDAN1D:29;
set E1 = ((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;
set i = len (Gauge C,n);
A3: Lower_Seq C,n = (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) :- (E-max (L~ (Cage C,n))) by JORDAN1E:def 2
.= <*(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 FINSEQ_5:def 2 ;
A4: Cage C,n is_sequence_on Gauge C,n by JORDAN9:def 1;
then Rotate (Cage C,n),(W-min (L~ (Cage C,n))) is_sequence_on Gauge C,n by REVROT_1:34;
then A5: (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))))) is_sequence_on Gauge C,n by JORDAN8:5;
A6: for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (Gauge C,n) & [i2,j2] in Indices (Gauge C,n) & E-max (L~ (Cage C,n)) = (Gauge C,n) * i1,j1 & ((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 = (Gauge C,n) * i2,j2 holds
(abs (i2 - i1)) + (abs (j2 - j1)) = 1

proof

set en = (E-max (L~ (Cage C,n))) .. (Cage C,n);
let i1, j1, i2, j2 be Element of NAT ; :: thesis: ( [i1,j1] in Indices (Gauge C,n) & [i2,j2] in Indices (Gauge C,n) & E-max (L~ (Cage C,n)) = (Gauge C,n) * i1,j1 & ((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 = (Gauge C,n) * i2,j2 implies (abs (i2 - i1)) + (abs (j2 - j1)) = 1 )
assume A7: ( [i1,j1] in Indices (Gauge C,n) & [i2,j2] in Indices (Gauge C,n) & E-max (L~ (Cage C,n)) = (Gauge C,n) * i1,j1 & ((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 = (Gauge C,n) * i2,j2 ) ; :: thesis: (abs (i2 - i1)) + (abs (j2 - j1)) = 1
(E-max (L~ (Cage C,n))) .. (Cage C,n) < len (Cage C,n) by SPRECT_5:17;
then ( 1 <= ((E-max (L~ (Cage C,n))) .. (Cage C,n)) + 1 & ((E-max (L~ (Cage C,n))) .. (Cage C,n)) + 1 <= len (Cage C,n) ) by NAT_1:11, NAT_1:13;
then A8: ((E-max (L~ (Cage C,n))) .. (Cage C,n)) + 1 in dom (Cage C,n) by FINSEQ_3:27;
A9: W-min (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:47;
A10: (Cage C,n) /. 1 = N-min (L~ (Cage C,n)) by JORDAN9:34;
then (E-max (L~ (Cage C,n))) .. (Cage C,n) < (E-min (L~ (Cage C,n))) .. (Cage C,n) by SPRECT_2:75;
then (E-max (L~ (Cage C,n))) .. (Cage C,n) < (S-max (L~ (Cage C,n))) .. (Cage C,n) by A10, SPRECT_2:76, XXREAL_0:2;
then (E-max (L~ (Cage C,n))) .. (Cage C,n) < (S-min (L~ (Cage C,n))) .. (Cage C,n) by A10, SPRECT_2:77, XXREAL_0:2;
then A11: (E-max (L~ (Cage C,n))) .. (Cage C,n) < (W-min (L~ (Cage C,n))) .. (Cage C,n) by A10, SPRECT_2:78, XXREAL_0:2;
then A12: ((E-max (L~ (Cage C,n))) .. (Cage C,n)) + 1 <= (W-min (L~ (Cage C,n))) .. (Cage C,n) by NAT_1:13;
A13: (len (Cage C,n)) - ((W-min (L~ (Cage C,n))) .. (Cage C,n)) > 0 by SPRECT_5:21, XREAL_1:52;
then A14: (((E-max (L~ (Cage C,n))) .. (Cage C,n)) + 1) + ((len (Cage C,n)) - ((W-min (L~ (Cage C,n))) .. (Cage C,n))) >= 0 + 0 ;
A15: E-max (L~ (Cage C,n)) in rng (Cage C,n) by SPRECT_2:50;
then 1 <= (E-max (L~ (Cage C,n))) .. (Cage C,n) by FINSEQ_4:31;
then A16: 1 < ((E-max (L~ (Cage C,n))) .. (Cage C,n)) + 1 by NAT_1:13;
E-max (L~ (Cage C,n)) in rng (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) by A15, FINSEQ_6:96, SPRECT_2:47;
then A17: (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 FINSEQ_4:31;

now

assume (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)))) ; :: thesis: contradiction
then (E-max (L~ (Cage C,n))) .. (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) = len (Cage C,n) by REVROT_1:14;
then len (Upper_Seq C,n) = len (Cage C,n) by JORDAN1E:12;
then (len (Cage C,n)) + (len (Lower_Seq C,n)) = (len (Cage C,n)) + 1 by JORDAN1E:14;
hence contradiction by JORDAN1E:19; :: thesis: verum

end;

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 A17, XXREAL_0:1;
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 (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))))) <= (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:11;
then 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 A17, RFINSEQ:def 2;
then 1 in dom ((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 FINSEQ_3:27;
then ((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 = (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:30
.= (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. ((((len (Cage C,n)) + ((E-max (L~ (Cage C,n))) .. (Cage C,n))) - ((W-min (L~ (Cage C,n))) .. (Cage C,n))) + 1) by A15, A9, A11, SPRECT_5:10
.= (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. ((((E-max (L~ (Cage C,n))) .. (Cage C,n)) + ((len (Cage C,n)) - ((W-min (L~ (Cage C,n))) .. (Cage C,n)))) + 1)
.= (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. ((((E-max (L~ (Cage C,n))) .. (Cage C,n)) + ((len (Cage C,n)) -' ((W-min (L~ (Cage C,n))) .. (Cage C,n)))) + 1) by A13, XREAL_0:def 2
.= (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. ((((E-max (L~ (Cage C,n))) .. (Cage C,n)) + 1) + ((len (Cage C,n)) -' ((W-min (L~ (Cage C,n))) .. (Cage C,n))))
.= (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. ((((E-max (L~ (Cage C,n))) .. (Cage C,n)) + 1) + ((len (Cage C,n)) - ((W-min (L~ (Cage C,n))) .. (Cage C,n)))) by A13, XREAL_0:def 2
.= (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. (((((E-max (L~ (Cage C,n))) .. (Cage C,n)) + 1) + (len (Cage C,n))) - ((W-min (L~ (Cage C,n))) .. (Cage C,n)))
.= (Rotate (Cage C,n),(W-min (L~ (Cage C,n)))) /. (((((E-max (L~ (Cage C,n))) .. (Cage C,n)) + 1) + (len (Cage C,n))) -' ((W-min (L~ (Cage C,n))) .. (Cage C,n))) by A14, XREAL_0:def 2 ;
then A18: ((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 = (Cage C,n) /. (((E-max (L~ (Cage C,n))) .. (Cage C,n)) + 1) by A9, A16, A12, REVROT_1:13;
( E-max (L~ (Cage C,n)) = (Cage C,n) /. ((E-max (L~ (Cage C,n))) .. (Cage C,n)) & (E-max (L~ (Cage C,n))) .. (Cage C,n) in dom (Cage C,n) ) by A15, FINSEQ_4:30, FINSEQ_5:41;
then (abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A4, A7, A8, A18, GOBOARD1:def 11;
then (abs (i1 - i2)) + (abs (j2 - j1)) = 1 by UNIFORM1:13;
hence (abs (i2 - i1)) + (abs (j2 - j1)) = 1 by UNIFORM1:13; :: thesis: verum

end;

len (Gauge C,n) >= 4 by JORDAN8:13;
then 1 <= len (Gauge C,n) by XXREAL_0:2;
then [(len (Gauge C,n)),j] in Indices (Gauge C,n) by A1, MATRIX_1:37;
hence Lower_Seq C,n is_sequence_on Gauge C,n by A5, A2, A6, A3, Th11; :: thesis: verum