let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); for n being Nat holds Lower_Seq (C,n) is_sequence_on Gauge (C,n)
let n be Nat; Lower_Seq (C,n) is_sequence_on Gauge (C,n)
consider j being 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:25;
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:2;
A6:
for i1, j1, i2, j2 being 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
|.(i2 - i1).| + |.(j2 - j1).| = 1
proof
set en =
(E-max (L~ (Cage (C,n)))) .. (Cage (C,n));
let i1,
j1,
i2,
j2 be
Nat;
( [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 |.(i2 - i1).| + |.(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) )
;
|.(i2 - i1).| + |.(j2 - j1).| = 1
(E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < len (Cage (C,n))
by SPRECT_5:16;
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:25;
A9:
W-min (L~ (Cage (C,n))) in rng (Cage (C,n))
by SPRECT_2:43;
A10:
(Cage (C,n)) /. 1
= N-min (L~ (Cage (C,n)))
by JORDAN9:32;
then
(E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (E-min (L~ (Cage (C,n)))) .. (Cage (C,n))
by SPRECT_2:71;
then
(E-max (L~ (Cage (C,n)))) .. (Cage (C,n)) < (S-max (L~ (Cage (C,n)))) .. (Cage (C,n))
by A10, SPRECT_2:72, 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:73, 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:74, 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:20, XREAL_1:50;
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:46;
then
1
<= (E-max (L~ (Cage (C,n)))) .. (Cage (C,n))
by FINSEQ_4:21;
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:90, SPRECT_2:43;
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:21;
now not (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))))))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))))))
;
contradictionthen
(E-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) = len (Cage (C,n))
by FINSEQ_6:179;
then
len (Upper_Seq (C,n)) = len (Cage (C,n))
by JORDAN1E:8;
then
(len (Cage (C,n))) + (len (Lower_Seq (C,n))) = (len (Cage (C,n))) + 1
by JORDAN1E:10;
hence
contradiction
by JORDAN1E:15;
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:9;
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 1;
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:25;
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:27
.=
(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:9
.=
(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, FINSEQ_6:178;
(
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:20, FINSEQ_5:38;
then
|.(i1 - i2).| + |.(j1 - j2).| = 1
by A4, A7, A8, A18, GOBOARD1:def 9;
then
|.(i1 - i2).| + |.(j2 - j1).| = 1
by UNIFORM1:11;
hence
|.(i2 - i1).| + |.(j2 - j1).| = 1
by UNIFORM1:11;
verum
end;
len (Gauge (C,n)) >= 4
by JORDAN8:10;
then
1 <= len (Gauge (C,n))
by XXREAL_0:2;
then
[(len (Gauge (C,n))),j] in Indices (Gauge (C,n))
by A1, MATRIX_0:30;
hence
Lower_Seq (C,n) is_sequence_on Gauge (C,n)
by A5, A2, A6, A3, Th11; verum