let n be Nat; for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i being Nat st 1 < i & i <= len (Gauge (C,n)) holds
not (Gauge (C,n)) * (i,1) in rng (Upper_Seq (C,n))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); for i being Nat st 1 < i & i <= len (Gauge (C,n)) holds
not (Gauge (C,n)) * (i,1) in rng (Upper_Seq (C,n))
let i be Nat; ( 1 < i & i <= len (Gauge (C,n)) implies not (Gauge (C,n)) * (i,1) in rng (Upper_Seq (C,n)) )
assume that
A1:
( 1 < i & i <= len (Gauge (C,n)) )
and
A2:
(Gauge (C,n)) * (i,1) in rng (Upper_Seq (C,n))
; contradiction
consider i2 being Nat such that
A3:
i2 in dom (Upper_Seq (C,n))
and
A4:
(Upper_Seq (C,n)) . i2 = (Gauge (C,n)) * (i,1)
by A2, FINSEQ_2:10;
reconsider i2 = i2 as Nat ;
A5:
( 1 <= i2 & i2 <= len (Upper_Seq (C,n)) )
by A3, FINSEQ_3:25;
set f = Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))));
set i1 = (N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n));
A6:
( E-max (L~ (Cage (C,n))) in rng (Cage (C,n)) & rng (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) = rng (Cage (C,n)) )
by FINSEQ_6:90, SPRECT_2:43, SPRECT_2:46;
W-min (L~ (Cage (C,n))) in rng (Cage (C,n))
by SPRECT_2:43;
then A7:
(Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) /. 1 = W-min (L~ (Cage (C,n)))
by FINSEQ_6:92;
L~ (Cage (C,n)) = L~ (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n))))))
by REVROT_1:33;
then A8:
( (N-min (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) < (N-max (L~ (Cage (C,n)))) .. (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) & (N-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 A7, SPRECT_5:24, SPRECT_5:25;
(E-max (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) = len (Upper_Seq (C,n))
by Th24;
then
(N-max (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) <= len (Upper_Seq (C,n))
by Th23;
then A9:
(N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) < len (Upper_Seq (C,n))
by Th22, XXREAL_0:2;
3 <= len (Lower_Seq (C,n))
by JORDAN1E:15;
then A10:
2 <= len (Lower_Seq (C,n))
by XXREAL_0:2;
A11:
len (Gauge (C,n)) = width (Gauge (C,n))
by JORDAN8:def 1;
4 <= len (Gauge (C,n))
by JORDAN8:10;
then A12:
1 <= len (Gauge (C,n))
by XXREAL_0:2;
( (W-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) = 1 & (W-max (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) <= (N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) )
by Th19, Th21;
then A13:
(N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) > 1
by Th20, XXREAL_0:2;
then A14:
(N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) in dom (Upper_Seq (C,n))
by A9, FINSEQ_3:25;
( Upper_Seq (C,n) = (Rotate ((Cage (C,n)),(W-min (L~ (Cage (C,n)))))) -: (E-max (L~ (Cage (C,n)))) & N-min (L~ (Cage (C,n))) in rng (Cage (C,n)) )
by JORDAN1E:def 1, SPRECT_2:39;
then A15:
N-min (L~ (Cage (C,n))) in rng (Upper_Seq (C,n))
by A6, A8, FINSEQ_5:46, XXREAL_0:2;
then A16:
(Upper_Seq (C,n)) /. ((N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n))) = N-min (L~ (Cage (C,n)))
by FINSEQ_5:38;
A17:
( (N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) in NAT & i2 in NAT )
by ORDINAL1:def 12;
A18:
(N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) <> i2
proof
assume
(N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)) = i2
;
contradiction
then
(Gauge (C,n)) * (
i,1)
= N-min (L~ (Cage (C,n)))
by A4, A14, A16, PARTFUN1:def 6;
then
((Gauge (C,n)) * (i,1)) `2 = N-bound (L~ (Cage (C,n)))
by EUCLID:52;
then
S-bound (L~ (Cage (C,n))) = N-bound (L~ (Cage (C,n)))
by A1, JORDAN1A:72;
hence
contradiction
by SPRECT_1:16;
verum
end;
then
mid ((Upper_Seq (C,n)),((N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n))),i2) is being_S-Seq
by A13, A9, A5, JORDAN3:6, A17;
then reconsider h1 = mid ((Upper_Seq (C,n)),((N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n))),i2) as one-to-one special FinSequence of (TOP-REAL 2) ;
set h = Rev h1;
A19:
len h1 = len (Rev h1)
by FINSEQ_5:def 3;
then A20:
not h1 is empty
by A3, A14, SPRECT_2:5;
then A21: ((Rev h1) /. (len (Rev h1))) `2 =
(h1 /. 1) `2
by A19, FINSEQ_5:65
.=
((Upper_Seq (C,n)) /. ((N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n)))) `2
by A3, A14, SPRECT_2:8
.=
(N-min (L~ (Cage (C,n)))) `2
by A15, FINSEQ_5:38
.=
N-bound (L~ (Cage (C,n)))
by EUCLID:52
;
h1 is_in_the_area_of Cage (C,n)
by A3, A14, JORDAN1E:17, SPRECT_2:22;
then A22:
Rev h1 is_in_the_area_of Cage (C,n)
by SPRECT_3:51;
((Rev h1) /. 1) `2 =
(h1 /. (len h1)) `2
by A20, FINSEQ_5:65
.=
((Upper_Seq (C,n)) /. i2) `2
by A3, A14, SPRECT_2:9
.=
((Gauge (C,n)) * (i,1)) `2
by A3, A4, PARTFUN1:def 6
.=
S-bound (L~ (Cage (C,n)))
by A1, JORDAN1A:72
;
then A23:
( Rev (Lower_Seq (C,n)) is special & Rev h1 is_a_v.c._for Cage (C,n) )
by A22, A21, SPRECT_2:def 3;
len (Rev h1) >= 1
by A3, A14, A19, SPRECT_2:5;
then
len (Rev h1) > 1
by A3, A14, A18, A19, SPRECT_2:6, XXREAL_0:1;
then A24:
1 + 1 <= len (Rev h1)
by NAT_1:13;
( len (Lower_Seq (C,n)) = len (Rev (Lower_Seq (C,n))) & Rev h1 is special )
by FINSEQ_5:def 3, SPPOL_2:40;
then
( L~ (Rev (Lower_Seq (C,n))) = L~ (Lower_Seq (C,n)) & L~ (Rev (Lower_Seq (C,n))) meets L~ (Rev h1) )
by A10, A24, A23, Th41, SPPOL_2:22, SPRECT_2:29;
then consider x being object such that
A25:
x in L~ (Lower_Seq (C,n))
and
A26:
x in L~ (Rev h1)
by XBOOLE_0:3;
A27:
L~ (Rev h1) = L~ h1
by SPPOL_2:22;
L~ (mid ((Upper_Seq (C,n)),((N-min (L~ (Cage (C,n)))) .. (Upper_Seq (C,n))),i2)) c= L~ (Upper_Seq (C,n))
by A13, A9, A5, JORDAN4:35;
then
x in (L~ (Upper_Seq (C,n))) /\ (L~ (Lower_Seq (C,n)))
by A25, A26, A27, XBOOLE_0:def 4;
then A28:
x in {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))}
by JORDAN1E:16;
per cases
( x = W-min (L~ (Cage (C,n))) or x = E-max (L~ (Cage (C,n))) )
by A28, TARSKI:def 2;
suppose
x = W-min (L~ (Cage (C,n)))
;
contradictionthen
x = (Upper_Seq (C,n)) /. 1
by JORDAN1F:5;
then
i2 = 1
by A13, A9, A5, A26, A27, Th37;
then
(Upper_Seq (C,n)) /. 1
= (Gauge (C,n)) * (
i,1)
by A3, A4, PARTFUN1:def 6;
then
W-min (L~ (Cage (C,n))) = (Gauge (C,n)) * (
i,1)
by JORDAN1F:5;
then ((Gauge (C,n)) * (i,1)) `1 =
W-bound (L~ (Cage (C,n)))
by EUCLID:52
.=
((Gauge (C,n)) * (1,1)) `1
by A12, JORDAN1A:73
;
hence
contradiction
by A1, A12, A11, GOBOARD5:3;
verum end; suppose
x = E-max (L~ (Cage (C,n)))
;
contradictionthen
x = (Upper_Seq (C,n)) /. (len (Upper_Seq (C,n)))
by JORDAN1F:7;
then
i2 = len (Upper_Seq (C,n))
by A13, A9, A5, A26, A27, Th38;
then
(Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) = (Gauge (C,n)) * (
i,1)
by A3, A4, PARTFUN1:def 6;
then A29:
E-max (L~ (Cage (C,n))) = (Gauge (C,n)) * (
i,1)
by JORDAN1F:7;
(SE-corner (L~ (Cage (C,n)))) `2 <= (E-min (L~ (Cage (C,n)))) `2
by PSCOMP_1:46;
then
(SE-corner (L~ (Cage (C,n)))) `2 < (E-max (L~ (Cage (C,n)))) `2
by SPRECT_2:53, XXREAL_0:2;
then
S-bound (L~ (Cage (C,n))) < ((Gauge (C,n)) * (i,1)) `2
by A29, EUCLID:52;
hence
contradiction
by A1, JORDAN1A:72;
verum end; end;