let n be Nat; for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j being Nat st 1 <= i & i <= len (Gauge (C,n)) & 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * (i,j) in L~ (Cage (C,n)) holds
LSeg (((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))) meets L~ (Upper_Seq (C,n))
let C be connected compact non horizontal non vertical Subset of (TOP-REAL 2); for i, j being Nat st 1 <= i & i <= len (Gauge (C,n)) & 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * (i,j) in L~ (Cage (C,n)) holds
LSeg (((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))) meets L~ (Upper_Seq (C,n))
let i, j be Nat; ( 1 <= i & i <= len (Gauge (C,n)) & 1 <= j & j <= width (Gauge (C,n)) & (Gauge (C,n)) * (i,j) in L~ (Cage (C,n)) implies LSeg (((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))) meets L~ (Upper_Seq (C,n)) )
set Gij = (Gauge (C,n)) * (i,j);
assume that
A1:
1 <= i
and
A2:
i <= len (Gauge (C,n))
and
A3:
1 <= j
and
A4:
j <= width (Gauge (C,n))
and
A5:
(Gauge (C,n)) * (i,j) in L~ (Cage (C,n))
; LSeg (((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))) meets L~ (Upper_Seq (C,n))
set NE = SW-corner (L~ (Cage (C,n)));
set v1 = L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)));
set wG = width (Gauge (C,n));
set lG = len (Gauge (C,n));
set Gv1 = <*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))));
set v = (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(SW-corner (L~ (Cage (C,n))))*>;
set h = mid ((Upper_Seq (C,n)),2,(len (Upper_Seq (C,n))));
A6:
L~ (Cage (C,n)) = (L~ (Lower_Seq (C,n))) \/ (L~ (Upper_Seq (C,n)))
by JORDAN1E:13;
A7:
len (Upper_Seq (C,n)) >= 3
by JORDAN1E:15;
A8:
len (Lower_Seq (C,n)) >= 3
by JORDAN1E:15;
A9:
len (Upper_Seq (C,n)) >= 2
by A7, XXREAL_0:2;
A10:
len (Upper_Seq (C,n)) >= 1
by A7, XXREAL_0:2;
A11:
len (Lower_Seq (C,n)) >= 1
by A8, XXREAL_0:2;
A12:
len (Gauge (C,n)) = width (Gauge (C,n))
by JORDAN8:def 1;
then
width (Gauge (C,n)) >= 4
by JORDAN8:10;
then A13:
1 <= width (Gauge (C,n))
by XXREAL_0:2;
A14:
((Gauge (C,n)) * (i,(width (Gauge (C,n))))) `2 = N-bound (L~ (Cage (C,n)))
by A1, A2, A12, JORDAN1A:70;
set Ema = E-max (L~ (Cage (C,n)));
now LSeg (((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))) meets L~ (Upper_Seq (C,n))per cases
( ( (Gauge (C,n)) * (i,j) in L~ (Lower_Seq (C,n)) & i = len (Gauge (C,n)) ) or ( (Gauge (C,n)) * (i,j) in L~ (Lower_Seq (C,n)) & (Gauge (C,n)) * (i,j) <> (Lower_Seq (C,n)) . (len (Lower_Seq (C,n))) & W-min (L~ (Cage (C,n))) <> SW-corner (L~ (Cage (C,n))) & i < len (Gauge (C,n)) ) or ( (Gauge (C,n)) * (i,j) in L~ (Lower_Seq (C,n)) & (Gauge (C,n)) * (i,j) <> (Lower_Seq (C,n)) . (len (Lower_Seq (C,n))) & W-min (L~ (Cage (C,n))) = SW-corner (L~ (Cage (C,n))) & i < len (Gauge (C,n)) ) or (Gauge (C,n)) * (i,j) in L~ (Upper_Seq (C,n)) or ( (Gauge (C,n)) * (i,j) in L~ (Lower_Seq (C,n)) & (Gauge (C,n)) * (i,j) = (Lower_Seq (C,n)) . (len (Lower_Seq (C,n))) ) )
by A2, A5, A6, XBOOLE_0:def 3, XXREAL_0:1;
suppose A15:
(
(Gauge (C,n)) * (
i,
j)
in L~ (Lower_Seq (C,n)) &
i = len (Gauge (C,n)) )
;
LSeg (((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))) meets L~ (Upper_Seq (C,n))set G11 =
(Gauge (C,n)) * (
(len (Gauge (C,n))),
(width (Gauge (C,n))));
A16:
((Gauge (C,n)) * ((len (Gauge (C,n))),(width (Gauge (C,n))))) `1 = E-bound (L~ (Cage (C,n)))
by A1, A12, A15, JORDAN1A:71;
A17:
(E-max (L~ (Cage (C,n)))) `1 = E-bound (L~ (Cage (C,n)))
by EUCLID:52;
A18:
N-bound (L~ (Cage (C,n))) = ((Gauge (C,n)) * ((len (Gauge (C,n))),(width (Gauge (C,n))))) `2
by A1, A12, A15, JORDAN1A:70;
E-max (L~ (Cage (C,n))) in L~ (Cage (C,n))
by SPRECT_1:14;
then A19:
((Gauge (C,n)) * ((len (Gauge (C,n))),(width (Gauge (C,n))))) `2 >= (E-max (L~ (Cage (C,n)))) `2
by A18, PSCOMP_1:24;
A20:
((Gauge (C,n)) * (i,j)) `1 = E-bound (L~ (Cage (C,n)))
by A3, A4, A12, A15, JORDAN1A:71;
then
(Gauge (C,n)) * (
i,
j)
in E-most (L~ (Cage (C,n)))
by A5, SPRECT_2:13;
then
(E-max (L~ (Cage (C,n)))) `2 >= ((Gauge (C,n)) * (i,j)) `2
by PSCOMP_1:47;
then A21:
E-max (L~ (Cage (C,n))) in LSeg (
((Gauge (C,n)) * ((len (Gauge (C,n))),(width (Gauge (C,n))))),
((Gauge (C,n)) * ((len (Gauge (C,n))),j)))
by A15, A16, A17, A19, A20, GOBOARD7:7;
A22:
rng (Upper_Seq (C,n)) c= L~ (Upper_Seq (C,n))
by A7, SPPOL_2:18, XXREAL_0:2;
(Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) = E-max (L~ (Cage (C,n)))
by JORDAN1F:7;
then
E-max (L~ (Cage (C,n))) in rng (Upper_Seq (C,n))
by FINSEQ_6:168;
hence
LSeg (
((Gauge (C,n)) * (i,(width (Gauge (C,n))))),
((Gauge (C,n)) * (i,j)))
meets L~ (Upper_Seq (C,n))
by A15, A21, A22, XBOOLE_0:3;
verum end; suppose A23:
(
(Gauge (C,n)) * (
i,
j)
in L~ (Lower_Seq (C,n)) &
(Gauge (C,n)) * (
i,
j)
<> (Lower_Seq (C,n)) . (len (Lower_Seq (C,n))) &
W-min (L~ (Cage (C,n))) <> SW-corner (L~ (Cage (C,n))) &
i < len (Gauge (C,n)) )
;
LSeg (((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))) meets L~ (Upper_Seq (C,n))then A24:
not
L_Cut (
(Lower_Seq (C,n)),
((Gauge (C,n)) * (i,j))) is
empty
by JORDAN1E:3;
then A25:
0 + 1
<= len (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))
by NAT_1:13;
then A26:
1
in dom (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))
by FINSEQ_3:25;
A27:
len (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) in dom (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))
by A25, FINSEQ_3:25;
A28:
len (Lower_Seq (C,n)) in dom (Lower_Seq (C,n))
by A11, FINSEQ_3:25;
A29:
(L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) /. (len (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) =
(L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) . (len (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))))
by A27, PARTFUN1:def 6
.=
(Lower_Seq (C,n)) . (len (Lower_Seq (C,n)))
by A23, JORDAN1B:4
.=
(Lower_Seq (C,n)) /. (len (Lower_Seq (C,n)))
by A28, PARTFUN1:def 6
.=
W-min (L~ (Cage (C,n)))
by JORDAN1F:8
;
then A30:
(<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) /. (len (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))))) = W-min (L~ (Cage (C,n)))
by A24, SPRECT_3:1;
A31:
(L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) /. 1 =
(L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) . 1
by A26, PARTFUN1:def 6
.=
(Gauge (C,n)) * (
i,
j)
by A23, JORDAN3:23
;
then A32:
((L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) ^ <*(SW-corner (L~ (Cage (C,n))))*>) /. 1
= (Gauge (C,n)) * (
i,
j)
by A25, BOOLMARK:7;
A33:
1
+ (len (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) >= 1
+ 1
by A25, XREAL_1:7;
len ((<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(SW-corner (L~ (Cage (C,n))))*>) =
(len (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))))) + 1
by FINSEQ_2:16
.=
(1 + (len (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))))) + 1
by FINSEQ_5:8
;
then
2
< len ((<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(SW-corner (L~ (Cage (C,n))))*>)
by A33, NAT_1:13;
then A34:
2
< len (Rev ((<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(SW-corner (L~ (Cage (C,n))))*>))
by FINSEQ_5:def 3;
S-bound (L~ (Cage (C,n))) < N-bound (L~ (Cage (C,n)))
by SPRECT_1:32;
then
SW-corner (L~ (Cage (C,n))) <> (Gauge (C,n)) * (
i,
(width (Gauge (C,n))))
by A14, EUCLID:52;
then
not
SW-corner (L~ (Cage (C,n))) in {((Gauge (C,n)) * (i,(width (Gauge (C,n)))))}
by TARSKI:def 1;
then A35:
not
SW-corner (L~ (Cage (C,n))) in rng <*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*>
by FINSEQ_1:39;
len (Cage (C,n)) > 4
by GOBOARD7:34;
then A36:
rng (Cage (C,n)) c= L~ (Cage (C,n))
by SPPOL_2:18, XXREAL_0:2;
A37:
not
SW-corner (L~ (Cage (C,n))) in rng (Cage (C,n))
proof
assume A38:
SW-corner (L~ (Cage (C,n))) in rng (Cage (C,n))
;
contradiction
A39:
(SW-corner (L~ (Cage (C,n)))) `1 = W-bound (L~ (Cage (C,n)))
by EUCLID:52;
A40:
(SW-corner (L~ (Cage (C,n)))) `2 = S-bound (L~ (Cage (C,n)))
by EUCLID:52;
then
(SW-corner (L~ (Cage (C,n)))) `2 <= N-bound (L~ (Cage (C,n)))
by SPRECT_1:22;
then
SW-corner (L~ (Cage (C,n))) in { p where p is Point of (TOP-REAL 2) : ( p `1 = W-bound (L~ (Cage (C,n))) & p `2 <= N-bound (L~ (Cage (C,n))) & p `2 >= S-bound (L~ (Cage (C,n))) ) }
by A39, A40;
then
SW-corner (L~ (Cage (C,n))) in LSeg (
(SW-corner (L~ (Cage (C,n)))),
(NW-corner (L~ (Cage (C,n)))))
by SPRECT_1:26;
then
SW-corner (L~ (Cage (C,n))) in (LSeg ((SW-corner (L~ (Cage (C,n)))),(NW-corner (L~ (Cage (C,n)))))) /\ (L~ (Cage (C,n)))
by A36, A38, XBOOLE_0:def 4;
then A41:
(SW-corner (L~ (Cage (C,n)))) `2 >= (W-min (L~ (Cage (C,n)))) `2
by PSCOMP_1:31;
(W-min (L~ (Cage (C,n)))) `2 >= (SW-corner (L~ (Cage (C,n)))) `2
by PSCOMP_1:30;
then A42:
(W-min (L~ (Cage (C,n)))) `2 = (SW-corner (L~ (Cage (C,n)))) `2
by A41, XXREAL_0:1;
(W-min (L~ (Cage (C,n)))) `1 = (SW-corner (L~ (Cage (C,n)))) `1
by PSCOMP_1:29;
hence
contradiction
by A23, A42, TOPREAL3:6;
verum
end; now not SW-corner (L~ (Cage (C,n))) in rng (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))per cases
( (Gauge (C,n)) * (i,j) <> (Lower_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1) or (Gauge (C,n)) * (i,j) = (Lower_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1) )
;
suppose
(Gauge (C,n)) * (
i,
j)
<> (Lower_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1)
;
not SW-corner (L~ (Cage (C,n))) in rng (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))then
L_Cut (
(Lower_Seq (C,n)),
((Gauge (C,n)) * (i,j)))
= <*((Gauge (C,n)) * (i,j))*> ^ (mid ((Lower_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1),(len (Lower_Seq (C,n)))))
by JORDAN3:def 3;
then
rng (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) = (rng <*((Gauge (C,n)) * (i,j))*>) \/ (rng (mid ((Lower_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1),(len (Lower_Seq (C,n))))))
by FINSEQ_1:31;
then A43:
rng (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) = {((Gauge (C,n)) * (i,j))} \/ (rng (mid ((Lower_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1),(len (Lower_Seq (C,n))))))
by FINSEQ_1:38;
not
SW-corner (L~ (Cage (C,n))) in L~ (Cage (C,n))
proof
assume
SW-corner (L~ (Cage (C,n))) in L~ (Cage (C,n))
;
contradiction
then consider i being
Nat such that A44:
1
<= i
and A45:
i + 1
<= len (Cage (C,n))
and A46:
SW-corner (L~ (Cage (C,n))) in LSeg (
((Cage (C,n)) /. i),
((Cage (C,n)) /. (i + 1)))
by SPPOL_2:14;
per cases
( ((Cage (C,n)) /. i) `1 = ((Cage (C,n)) /. (i + 1)) `1 or ((Cage (C,n)) /. i) `2 = ((Cage (C,n)) /. (i + 1)) `2 )
by A44, A45, TOPREAL1:def 5;
suppose A47:
((Cage (C,n)) /. i) `1 = ((Cage (C,n)) /. (i + 1)) `1
;
contradictionthen A48:
(SW-corner (L~ (Cage (C,n)))) `1 = ((Cage (C,n)) /. i) `1
by A46, GOBOARD7:5;
A49:
(SW-corner (L~ (Cage (C,n)))) `2 = S-bound (L~ (Cage (C,n)))
by EUCLID:52;
A50:
i < len (Cage (C,n))
by A45, NAT_1:13;
then A51:
((Cage (C,n)) /. i) `2 >= (SW-corner (L~ (Cage (C,n)))) `2
by A44, A49, JORDAN5D:11;
A52:
1
<= i + 1
by NAT_1:11;
then A53:
((Cage (C,n)) /. (i + 1)) `2 >= (SW-corner (L~ (Cage (C,n)))) `2
by A45, A49, JORDAN5D:11;
A54:
i in dom (Cage (C,n))
by A44, A50, FINSEQ_3:25;
A55:
i + 1
in dom (Cage (C,n))
by A45, A52, FINSEQ_3:25;
(
((Cage (C,n)) /. i) `2 <= ((Cage (C,n)) /. (i + 1)) `2 or
((Cage (C,n)) /. i) `2 >= ((Cage (C,n)) /. (i + 1)) `2 )
;
then
(
(SW-corner (L~ (Cage (C,n)))) `2 >= ((Cage (C,n)) /. (i + 1)) `2 or
(SW-corner (L~ (Cage (C,n)))) `2 >= ((Cage (C,n)) /. i) `2 )
by A46, TOPREAL1:4;
then
(
(SW-corner (L~ (Cage (C,n)))) `2 = ((Cage (C,n)) /. (i + 1)) `2 or
(SW-corner (L~ (Cage (C,n)))) `2 = ((Cage (C,n)) /. i) `2 )
by A51, A53, XXREAL_0:1;
then
(
SW-corner (L~ (Cage (C,n))) = (Cage (C,n)) /. (i + 1) or
SW-corner (L~ (Cage (C,n))) = (Cage (C,n)) /. i )
by A47, A48, TOPREAL3:6;
hence
contradiction
by A37, A54, A55, PARTFUN2:2;
verum end; suppose A56:
((Cage (C,n)) /. i) `2 = ((Cage (C,n)) /. (i + 1)) `2
;
contradictionthen A57:
(SW-corner (L~ (Cage (C,n)))) `2 = ((Cage (C,n)) /. i) `2
by A46, GOBOARD7:6;
A58:
(SW-corner (L~ (Cage (C,n)))) `1 = W-bound (L~ (Cage (C,n)))
by EUCLID:52;
A59:
i < len (Cage (C,n))
by A45, NAT_1:13;
then A60:
((Cage (C,n)) /. i) `1 >= (SW-corner (L~ (Cage (C,n)))) `1
by A44, A58, JORDAN5D:12;
A61:
1
<= i + 1
by NAT_1:11;
then A62:
((Cage (C,n)) /. (i + 1)) `1 >= (SW-corner (L~ (Cage (C,n)))) `1
by A45, A58, JORDAN5D:12;
A63:
i in dom (Cage (C,n))
by A44, A59, FINSEQ_3:25;
A64:
i + 1
in dom (Cage (C,n))
by A45, A61, FINSEQ_3:25;
(
((Cage (C,n)) /. i) `1 <= ((Cage (C,n)) /. (i + 1)) `1 or
((Cage (C,n)) /. i) `1 >= ((Cage (C,n)) /. (i + 1)) `1 )
;
then
(
(SW-corner (L~ (Cage (C,n)))) `1 >= ((Cage (C,n)) /. (i + 1)) `1 or
(SW-corner (L~ (Cage (C,n)))) `1 >= ((Cage (C,n)) /. i) `1 )
by A46, TOPREAL1:3;
then
(
(SW-corner (L~ (Cage (C,n)))) `1 = ((Cage (C,n)) /. (i + 1)) `1 or
(SW-corner (L~ (Cage (C,n)))) `1 = ((Cage (C,n)) /. i) `1 )
by A60, A62, XXREAL_0:1;
then
(
SW-corner (L~ (Cage (C,n))) = (Cage (C,n)) /. (i + 1) or
SW-corner (L~ (Cage (C,n))) = (Cage (C,n)) /. i )
by A56, A57, TOPREAL3:6;
hence
contradiction
by A37, A63, A64, PARTFUN2:2;
verum end; end;
end; then A65:
not
SW-corner (L~ (Cage (C,n))) in {((Gauge (C,n)) * (i,j))}
by A5, TARSKI:def 1;
A66:
rng (mid ((Lower_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1),(len (Lower_Seq (C,n))))) c= rng (Lower_Seq (C,n))
by FINSEQ_6:119;
rng (Lower_Seq (C,n)) c= rng (Cage (C,n))
by JORDAN1G:39;
then
rng (mid ((Lower_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1),(len (Lower_Seq (C,n))))) c= rng (Cage (C,n))
by A66;
then
not
SW-corner (L~ (Cage (C,n))) in rng (mid ((Lower_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1),(len (Lower_Seq (C,n)))))
by A37;
hence
not
SW-corner (L~ (Cage (C,n))) in rng (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))
by A43, A65, XBOOLE_0:def 3;
verum end; suppose
(Gauge (C,n)) * (
i,
j)
= (Lower_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1)
;
not SW-corner (L~ (Cage (C,n))) in rng (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))then
L_Cut (
(Lower_Seq (C,n)),
((Gauge (C,n)) * (i,j)))
= mid (
(Lower_Seq (C,n)),
((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1),
(len (Lower_Seq (C,n))))
by JORDAN3:def 3;
then A67:
rng (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) c= rng (Lower_Seq (C,n))
by FINSEQ_6:119;
rng (Lower_Seq (C,n)) c= rng (Cage (C,n))
by JORDAN1G:39;
then
rng (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) c= rng (Cage (C,n))
by A67;
hence
not
SW-corner (L~ (Cage (C,n))) in rng (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))
by A37;
verum end; end; end; then
not
SW-corner (L~ (Cage (C,n))) in (rng <*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*>) \/ (rng (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))))
by A35, XBOOLE_0:def 3;
then
not
SW-corner (L~ (Cage (C,n))) in rng (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))))
by FINSEQ_1:31;
then
rng (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) misses {(SW-corner (L~ (Cage (C,n))))}
by ZFMISC_1:50;
then A68:
rng (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) misses rng <*(SW-corner (L~ (Cage (C,n))))*>
by FINSEQ_1:38;
A69:
not
(Gauge (C,n)) * (
i,
(width (Gauge (C,n))))
in L~ (Lower_Seq (C,n))
by A1, A23, JORDAN1G:45;
rng (Lower_Seq (C,n)) c= L~ (Lower_Seq (C,n))
by A8, SPPOL_2:18, XXREAL_0:2;
then A70:
not
(Gauge (C,n)) * (
i,
(width (Gauge (C,n))))
in rng (Lower_Seq (C,n))
by A1, A23, JORDAN1G:45;
not
(Gauge (C,n)) * (
i,
(width (Gauge (C,n))))
in {((Gauge (C,n)) * (i,j))}
by A23, A69, TARSKI:def 1;
then A71:
not
(Gauge (C,n)) * (
i,
(width (Gauge (C,n))))
in rng <*((Gauge (C,n)) * (i,j))*>
by FINSEQ_1:38;
set ci =
mid (
(Lower_Seq (C,n)),
((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1),
(len (Lower_Seq (C,n))));
now not (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in rng (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))per cases
( (Gauge (C,n)) * (i,j) <> (Lower_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1) or (Gauge (C,n)) * (i,j) = (Lower_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1) )
;
suppose A72:
(Gauge (C,n)) * (
i,
j)
<> (Lower_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1)
;
not (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in rng (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))
rng (mid ((Lower_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1),(len (Lower_Seq (C,n))))) c= rng (Lower_Seq (C,n))
by FINSEQ_6:119;
then
not
(Gauge (C,n)) * (
i,
(width (Gauge (C,n))))
in rng (mid ((Lower_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1),(len (Lower_Seq (C,n)))))
by A70;
then
not
(Gauge (C,n)) * (
i,
(width (Gauge (C,n))))
in (rng <*((Gauge (C,n)) * (i,j))*>) \/ (rng (mid ((Lower_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1),(len (Lower_Seq (C,n))))))
by A71, XBOOLE_0:def 3;
then
not
(Gauge (C,n)) * (
i,
(width (Gauge (C,n))))
in rng (<*((Gauge (C,n)) * (i,j))*> ^ (mid ((Lower_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1),(len (Lower_Seq (C,n))))))
by FINSEQ_1:31;
hence
not
(Gauge (C,n)) * (
i,
(width (Gauge (C,n))))
in rng (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))
by A72, JORDAN3:def 3;
verum end; suppose
(Gauge (C,n)) * (
i,
j)
= (Lower_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1)
;
not (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in rng (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))then
L_Cut (
(Lower_Seq (C,n)),
((Gauge (C,n)) * (i,j)))
= mid (
(Lower_Seq (C,n)),
((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1),
(len (Lower_Seq (C,n))))
by JORDAN3:def 3;
then
rng (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) c= rng (Lower_Seq (C,n))
by FINSEQ_6:119;
hence
not
(Gauge (C,n)) * (
i,
(width (Gauge (C,n))))
in rng (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))
by A70;
verum end; end; end; then
{((Gauge (C,n)) * (i,(width (Gauge (C,n)))))} misses rng (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))
by ZFMISC_1:50;
then A73:
rng <*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> misses rng (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))
by FINSEQ_1:38;
A74:
<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> is
one-to-one
by FINSEQ_3:93;
A75:
L_Cut (
(Lower_Seq (C,n)),
((Gauge (C,n)) * (i,j))) is
being_S-Seq
by A23, JORDAN3:34;
then A76:
<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) is
one-to-one
by A73, A74, FINSEQ_3:91;
<*(SW-corner (L~ (Cage (C,n))))*> is
one-to-one
by FINSEQ_3:93;
then A77:
(<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(SW-corner (L~ (Cage (C,n))))*> is
one-to-one
by A68, A76, FINSEQ_3:91;
(<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. (len <*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*>)) `1 =
(<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. 1) `1
by FINSEQ_1:39
.=
((Gauge (C,n)) * (i,(width (Gauge (C,n))))) `1
by FINSEQ_4:16
.=
((Gauge (C,n)) * (i,1)) `1
by A1, A2, A13, GOBOARD5:2
.=
((L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) /. 1) `1
by A1, A2, A3, A4, A31, GOBOARD5:2
;
then A78:
<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) is
special
by A75, GOBOARD2:8;
((<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) /. (len (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))))) `1 =
(SW-corner (L~ (Cage (C,n)))) `1
by A30, PSCOMP_1:29
.=
(<*(SW-corner (L~ (Cage (C,n))))*> /. 1) `1
by FINSEQ_4:16
;
then
(<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(SW-corner (L~ (Cage (C,n))))*> is
special
by A78, GOBOARD2:8;
then A79:
Rev ((<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(SW-corner (L~ (Cage (C,n))))*>) is
special
by SPPOL_2:40;
A80:
len (Upper_Seq (C,n)) >= 2
+ 1
by JORDAN1E:15;
then A81:
len (Upper_Seq (C,n)) > 2
by NAT_1:13;
len (Upper_Seq (C,n)) > 1
by A80, XXREAL_0:2;
then A82:
mid (
(Upper_Seq (C,n)),2,
(len (Upper_Seq (C,n)))) is
S-Sequence_in_R2
by A81, JORDAN3:6;
then A83:
2
<= len (mid ((Upper_Seq (C,n)),2,(len (Upper_Seq (C,n)))))
by TOPREAL1:def 8;
3
<= len (Upper_Seq (C,n))
by JORDAN1E:15;
then
2
<= len (Upper_Seq (C,n))
by XXREAL_0:2;
then A84:
2
in dom (Upper_Seq (C,n))
by FINSEQ_3:25;
A85:
len (Upper_Seq (C,n)) in dom (Upper_Seq (C,n))
by FINSEQ_5:6;
then A86:
mid (
(Upper_Seq (C,n)),2,
(len (Upper_Seq (C,n))))
is_in_the_area_of Cage (
C,
n)
by A84, JORDAN1E:17, SPRECT_2:22;
(Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) = E-max (L~ (Cage (C,n)))
by JORDAN1F:7;
then
((Upper_Seq (C,n)) /. (len (Upper_Seq (C,n)))) `1 = E-bound (L~ (Cage (C,n)))
by EUCLID:52;
then A87:
((mid ((Upper_Seq (C,n)),2,(len (Upper_Seq (C,n))))) /. (len (mid ((Upper_Seq (C,n)),2,(len (Upper_Seq (C,n))))))) `1 = E-bound (L~ (Cage (C,n)))
by A84, A85, SPRECT_2:9;
((Upper_Seq (C,n)) /. (1 + 1)) `1 = W-bound (L~ (Cage (C,n)))
by JORDAN1G:31;
then
((mid ((Upper_Seq (C,n)),2,(len (Upper_Seq (C,n))))) /. 1) `1 = W-bound (L~ (Cage (C,n)))
by A84, A85, SPRECT_2:8;
then A88:
mid (
(Upper_Seq (C,n)),2,
(len (Upper_Seq (C,n))))
is_a_h.c._for Cage (
C,
n)
by A86, A87, SPRECT_2:def 2;
now for m being Nat st m in dom <*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> holds
( W-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `1 & (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `1 <= E-bound (L~ (Cage (C,n))) & S-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `2 & (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `2 <= N-bound (L~ (Cage (C,n))) )let m be
Nat;
( m in dom <*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> implies ( W-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `1 & (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `1 <= E-bound (L~ (Cage (C,n))) & S-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `2 & (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `2 <= N-bound (L~ (Cage (C,n))) ) )assume A89:
m in dom <*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*>
;
( W-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `1 & (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `1 <= E-bound (L~ (Cage (C,n))) & S-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `2 & (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `2 <= N-bound (L~ (Cage (C,n))) )then
m in Seg 1
by FINSEQ_1:38;
then
m = 1
by FINSEQ_1:2, TARSKI:def 1;
then
<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> . m = (Gauge (C,n)) * (
i,
(width (Gauge (C,n))))
by FINSEQ_1:40;
then A90:
<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m = (Gauge (C,n)) * (
i,
(width (Gauge (C,n))))
by A89, PARTFUN1:def 6;
((Gauge (C,n)) * (1,(width (Gauge (C,n))))) `1 <= ((Gauge (C,n)) * (i,(width (Gauge (C,n))))) `1
by A1, A2, A13, SPRECT_3:13;
hence
W-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `1
by A12, A13, A90, JORDAN1A:73;
( (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `1 <= E-bound (L~ (Cage (C,n))) & S-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `2 & (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `2 <= N-bound (L~ (Cage (C,n))) )
((Gauge (C,n)) * (i,(width (Gauge (C,n))))) `1 <= ((Gauge (C,n)) * ((len (Gauge (C,n))),(width (Gauge (C,n))))) `1
by A1, A2, A13, SPRECT_3:13;
hence
(<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `1 <= E-bound (L~ (Cage (C,n)))
by A12, A13, A90, JORDAN1A:71;
( S-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `2 & (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `2 <= N-bound (L~ (Cage (C,n))) )
(<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `2 = N-bound (L~ (Cage (C,n)))
by A1, A2, A12, A90, JORDAN1A:70;
hence
S-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `2
by SPRECT_1:22;
(<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `2 <= N-bound (L~ (Cage (C,n)))thus
(<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `2 <= N-bound (L~ (Cage (C,n)))
by A1, A2, A12, A90, JORDAN1A:70;
verum end; then A91:
<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> is_in_the_area_of Cage (
C,
n)
by SPRECT_2:def 1;
<*((Gauge (C,n)) * (i,j))*> is_in_the_area_of Cage (
C,
n)
by A23, JORDAN1E:18, SPRECT_3:46;
then
L_Cut (
(Lower_Seq (C,n)),
((Gauge (C,n)) * (i,j)))
is_in_the_area_of Cage (
C,
n)
by A23, JORDAN1E:18, SPRECT_3:56;
then A92:
<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) is_in_the_area_of Cage (
C,
n)
by A91, SPRECT_2:24;
<*(SW-corner (L~ (Cage (C,n))))*> is_in_the_area_of Cage (
C,
n)
by SPRECT_2:28;
then
(<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(SW-corner (L~ (Cage (C,n))))*> is_in_the_area_of Cage (
C,
n)
by A92, SPRECT_2:24;
then A93:
Rev ((<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(SW-corner (L~ (Cage (C,n))))*>) is_in_the_area_of Cage (
C,
n)
by SPRECT_3:51;
(<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(SW-corner (L~ (Cage (C,n))))*> = <*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ ((L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) ^ <*(SW-corner (L~ (Cage (C,n))))*>)
by FINSEQ_1:32;
then
((<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(SW-corner (L~ (Cage (C,n))))*>) /. 1
= (Gauge (C,n)) * (
i,
(width (Gauge (C,n))))
by FINSEQ_5:15;
then
(((<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(SW-corner (L~ (Cage (C,n))))*>) /. 1) `2 = N-bound (L~ (Cage (C,n)))
by A1, A2, A12, JORDAN1A:70;
then
((Rev ((<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(SW-corner (L~ (Cage (C,n))))*>)) /. (len ((<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(SW-corner (L~ (Cage (C,n))))*>))) `2 = N-bound (L~ (Cage (C,n)))
by FINSEQ_5:65;
then A94:
((Rev ((<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(SW-corner (L~ (Cage (C,n))))*>)) /. (len (Rev ((<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(SW-corner (L~ (Cage (C,n))))*>)))) `2 = N-bound (L~ (Cage (C,n)))
by FINSEQ_5:def 3;
len ((<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(SW-corner (L~ (Cage (C,n))))*>) = (len (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))))) + 1
by FINSEQ_2:16;
then
((<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(SW-corner (L~ (Cage (C,n))))*>) /. (len ((<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(SW-corner (L~ (Cage (C,n))))*>)) = SW-corner (L~ (Cage (C,n)))
by FINSEQ_4:67;
then
(((<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(SW-corner (L~ (Cage (C,n))))*>) /. (len ((<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(SW-corner (L~ (Cage (C,n))))*>))) `2 = S-bound (L~ (Cage (C,n)))
by EUCLID:52;
then
((Rev ((<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(SW-corner (L~ (Cage (C,n))))*>)) /. 1) `2 = S-bound (L~ (Cage (C,n)))
by FINSEQ_5:65;
then
Rev ((<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(SW-corner (L~ (Cage (C,n))))*>) is_a_v.c._for Cage (
C,
n)
by A93, A94, SPRECT_2:def 3;
then
L~ (mid ((Upper_Seq (C,n)),2,(len (Upper_Seq (C,n))))) meets L~ (Rev ((<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(SW-corner (L~ (Cage (C,n))))*>))
by A34, A77, A79, A82, A83, A88, SPRECT_2:29;
then
L~ (mid ((Upper_Seq (C,n)),2,(len (Upper_Seq (C,n))))) meets L~ ((<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(SW-corner (L~ (Cage (C,n))))*>)
by SPPOL_2:22;
then consider x being
object such that A95:
x in L~ (mid ((Upper_Seq (C,n)),2,(len (Upper_Seq (C,n)))))
and A96:
x in L~ ((<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(SW-corner (L~ (Cage (C,n))))*>)
by XBOOLE_0:3;
A97:
L~ (mid ((Upper_Seq (C,n)),2,(len (Upper_Seq (C,n))))) c= L~ (Upper_Seq (C,n))
by A9, A10, JORDAN4:35;
A98:
L~ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) c= L~ (Lower_Seq (C,n))
by A23, JORDAN3:42;
L~ ((<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) ^ <*(SW-corner (L~ (Cage (C,n))))*>) =
L~ (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ ((L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) ^ <*(SW-corner (L~ (Cage (C,n))))*>))
by FINSEQ_1:32
.=
(LSeg (((Gauge (C,n)) * (i,(width (Gauge (C,n))))),(((L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) ^ <*(SW-corner (L~ (Cage (C,n))))*>) /. 1))) \/ (L~ ((L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) ^ <*(SW-corner (L~ (Cage (C,n))))*>))
by SPPOL_2:20
.=
(LSeg (((Gauge (C,n)) * (i,(width (Gauge (C,n))))),(((L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) ^ <*(SW-corner (L~ (Cage (C,n))))*>) /. 1))) \/ ((L~ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) \/ (LSeg (((L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) /. (len (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))))),(SW-corner (L~ (Cage (C,n)))))))
by A24, SPPOL_2:19
;
then A99:
(
x in LSeg (
((Gauge (C,n)) * (i,(width (Gauge (C,n))))),
(((L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) ^ <*(SW-corner (L~ (Cage (C,n))))*>) /. 1)) or
x in (L~ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) \/ (LSeg (((L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) /. (len (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))))),(SW-corner (L~ (Cage (C,n)))))) )
by A96, XBOOLE_0:def 3;
(Upper_Seq (C,n)) /. 1
= W-min (L~ (Cage (C,n)))
by JORDAN1F:5;
then A100:
not
W-min (L~ (Cage (C,n))) in L~ (mid ((Upper_Seq (C,n)),2,(len (Upper_Seq (C,n)))))
by A81, JORDAN5B:16;
now L~ (Upper_Seq (C,n)) meets L~ <*((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))*>per cases
( x in LSeg (((Gauge (C,n)) * (i,(width (Gauge (C,n))))),(((L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) ^ <*(SW-corner (L~ (Cage (C,n))))*>) /. 1)) or x in L~ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) or x in LSeg (((L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) /. (len (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))))),(SW-corner (L~ (Cage (C,n))))) )
by A99, XBOOLE_0:def 3;
suppose
x in LSeg (
((Gauge (C,n)) * (i,(width (Gauge (C,n))))),
(((L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) ^ <*(SW-corner (L~ (Cage (C,n))))*>) /. 1))
;
L~ (Upper_Seq (C,n)) meets L~ <*((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))*>then
x in L~ <*((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))*>
by A32, SPPOL_2:21;
hence
L~ (Upper_Seq (C,n)) meets L~ <*((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))*>
by A95, A97, XBOOLE_0:3;
verum end; suppose A101:
x in L~ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))
;
L~ (Upper_Seq (C,n)) meets L~ <*((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))*>then
x in (L~ (Lower_Seq (C,n))) /\ (L~ (Upper_Seq (C,n)))
by A95, A97, A98, XBOOLE_0:def 4;
then
x in {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))}
by JORDAN1E:16;
then A102:
x = E-max (L~ (Cage (C,n)))
by A95, A100, TARSKI:def 2;
1
in dom (Lower_Seq (C,n))
by A11, FINSEQ_3:25;
then (Lower_Seq (C,n)) . 1 =
(Lower_Seq (C,n)) /. 1
by PARTFUN1:def 6
.=
E-max (L~ (Cage (C,n)))
by JORDAN1F:6
;
then
x = (Gauge (C,n)) * (
i,
j)
by A23, A101, A102, JORDAN1E:7;
then
x in LSeg (
((Gauge (C,n)) * (i,(width (Gauge (C,n))))),
((Gauge (C,n)) * (i,j)))
by RLTOPSP1:68;
then
x in L~ <*((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))*>
by SPPOL_2:21;
hence
L~ (Upper_Seq (C,n)) meets L~ <*((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))*>
by A95, A97, XBOOLE_0:3;
verum end; suppose A103:
x in LSeg (
((L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) /. (len (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))))),
(SW-corner (L~ (Cage (C,n)))))
;
L~ (Upper_Seq (C,n)) meets L~ <*((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))*>
x in L~ (Cage (C,n))
by A6, A95, A97, XBOOLE_0:def 3;
then
x in (LSeg ((W-min (L~ (Cage (C,n)))),(SW-corner (L~ (Cage (C,n)))))) /\ (L~ (Cage (C,n)))
by A29, A103, XBOOLE_0:def 4;
then
x in {(W-min (L~ (Cage (C,n))))}
by PSCOMP_1:35;
hence
L~ (Upper_Seq (C,n)) meets L~ <*((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))*>
by A95, A100, TARSKI:def 1;
verum end; end; end; then
L~ <*((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))*> meets L~ (Upper_Seq (C,n))
;
hence
LSeg (
((Gauge (C,n)) * (i,(width (Gauge (C,n))))),
((Gauge (C,n)) * (i,j)))
meets L~ (Upper_Seq (C,n))
by SPPOL_2:21;
verum end; suppose A104:
(
(Gauge (C,n)) * (
i,
j)
in L~ (Lower_Seq (C,n)) &
(Gauge (C,n)) * (
i,
j)
<> (Lower_Seq (C,n)) . (len (Lower_Seq (C,n))) &
W-min (L~ (Cage (C,n))) = SW-corner (L~ (Cage (C,n))) &
i < len (Gauge (C,n)) )
;
LSeg (((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))) meets L~ (Upper_Seq (C,n))then A105:
not
L_Cut (
(Lower_Seq (C,n)),
((Gauge (C,n)) * (i,j))) is
empty
by JORDAN1E:3;
then A106:
0 + 1
<= len (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))
by NAT_1:13;
then A107:
1
in dom (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))
by FINSEQ_3:25;
set v =
<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))));
A108:
len (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) in dom (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))
by A106, FINSEQ_3:25;
A109:
len (Lower_Seq (C,n)) in dom (Lower_Seq (C,n))
by A11, FINSEQ_3:25;
(L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) /. (len (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) =
(L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) . (len (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))))
by A108, PARTFUN1:def 6
.=
(Lower_Seq (C,n)) . (len (Lower_Seq (C,n)))
by A104, JORDAN1B:4
.=
(Lower_Seq (C,n)) /. (len (Lower_Seq (C,n)))
by A109, PARTFUN1:def 6
.=
W-min (L~ (Cage (C,n)))
by JORDAN1F:8
;
then A110:
(<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) /. (len (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))))) = W-min (L~ (Cage (C,n)))
by A105, SPRECT_3:1;
A111:
(L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) /. 1 =
(L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) . 1
by A107, PARTFUN1:def 6
.=
(Gauge (C,n)) * (
i,
j)
by A104, JORDAN3:23
;
1
+ (len (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) >= 1
+ 1
by A106, XREAL_1:7;
then
2
<= len (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))))
by FINSEQ_5:8;
then A112:
2
<= len (Rev (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))))
by FINSEQ_5:def 3;
A113:
not
(Gauge (C,n)) * (
i,
(width (Gauge (C,n))))
in L~ (Lower_Seq (C,n))
by A1, A104, JORDAN1G:45;
rng (Lower_Seq (C,n)) c= L~ (Lower_Seq (C,n))
by A8, SPPOL_2:18, XXREAL_0:2;
then A114:
not
(Gauge (C,n)) * (
i,
(width (Gauge (C,n))))
in rng (Lower_Seq (C,n))
by A1, A104, JORDAN1G:45;
not
(Gauge (C,n)) * (
i,
(width (Gauge (C,n))))
in {((Gauge (C,n)) * (i,j))}
by A104, A113, TARSKI:def 1;
then A115:
not
(Gauge (C,n)) * (
i,
(width (Gauge (C,n))))
in rng <*((Gauge (C,n)) * (i,j))*>
by FINSEQ_1:38;
set ci =
mid (
(Lower_Seq (C,n)),
((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1),
(len (Lower_Seq (C,n))));
now not (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in rng (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))per cases
( (Gauge (C,n)) * (i,j) <> (Lower_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1) or (Gauge (C,n)) * (i,j) = (Lower_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1) )
;
suppose A116:
(Gauge (C,n)) * (
i,
j)
<> (Lower_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1)
;
not (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in rng (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))
rng (mid ((Lower_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1),(len (Lower_Seq (C,n))))) c= rng (Lower_Seq (C,n))
by FINSEQ_6:119;
then
not
(Gauge (C,n)) * (
i,
(width (Gauge (C,n))))
in rng (mid ((Lower_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1),(len (Lower_Seq (C,n)))))
by A114;
then
not
(Gauge (C,n)) * (
i,
(width (Gauge (C,n))))
in (rng <*((Gauge (C,n)) * (i,j))*>) \/ (rng (mid ((Lower_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1),(len (Lower_Seq (C,n))))))
by A115, XBOOLE_0:def 3;
then
not
(Gauge (C,n)) * (
i,
(width (Gauge (C,n))))
in rng (<*((Gauge (C,n)) * (i,j))*> ^ (mid ((Lower_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1),(len (Lower_Seq (C,n))))))
by FINSEQ_1:31;
hence
not
(Gauge (C,n)) * (
i,
(width (Gauge (C,n))))
in rng (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))
by A116, JORDAN3:def 3;
verum end; suppose
(Gauge (C,n)) * (
i,
j)
= (Lower_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1)
;
not (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in rng (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))then
L_Cut (
(Lower_Seq (C,n)),
((Gauge (C,n)) * (i,j)))
= mid (
(Lower_Seq (C,n)),
((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1),
(len (Lower_Seq (C,n))))
by JORDAN3:def 3;
then
rng (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) c= rng (Lower_Seq (C,n))
by FINSEQ_6:119;
hence
not
(Gauge (C,n)) * (
i,
(width (Gauge (C,n))))
in rng (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))
by A114;
verum end; end; end; then
{((Gauge (C,n)) * (i,(width (Gauge (C,n)))))} misses rng (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))
by ZFMISC_1:50;
then A117:
rng <*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> misses rng (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))
by FINSEQ_1:38;
A118:
<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> is
one-to-one
by FINSEQ_3:93;
A119:
L_Cut (
(Lower_Seq (C,n)),
((Gauge (C,n)) * (i,j))) is
being_S-Seq
by A104, JORDAN3:34;
then A120:
<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) is
one-to-one
by A117, A118, FINSEQ_3:91;
(<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. (len <*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*>)) `1 =
(<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. 1) `1
by FINSEQ_1:39
.=
((Gauge (C,n)) * (i,(width (Gauge (C,n))))) `1
by FINSEQ_4:16
.=
((Gauge (C,n)) * (i,1)) `1
by A1, A2, A13, GOBOARD5:2
.=
((L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) /. 1) `1
by A1, A2, A3, A4, A111, GOBOARD5:2
;
then
<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) is
special
by A119, GOBOARD2:8;
then A121:
Rev (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) is
special
by SPPOL_2:40;
A122:
len (Upper_Seq (C,n)) >= 2
+ 1
by JORDAN1E:15;
then A123:
len (Upper_Seq (C,n)) > 2
by NAT_1:13;
len (Upper_Seq (C,n)) > 1
by A122, XXREAL_0:2;
then A124:
mid (
(Upper_Seq (C,n)),2,
(len (Upper_Seq (C,n)))) is
S-Sequence_in_R2
by A123, JORDAN3:6;
then A125:
2
<= len (mid ((Upper_Seq (C,n)),2,(len (Upper_Seq (C,n)))))
by TOPREAL1:def 8;
3
<= len (Upper_Seq (C,n))
by JORDAN1E:15;
then
2
<= len (Upper_Seq (C,n))
by XXREAL_0:2;
then A126:
2
in dom (Upper_Seq (C,n))
by FINSEQ_3:25;
A127:
len (Upper_Seq (C,n)) in dom (Upper_Seq (C,n))
by FINSEQ_5:6;
then A128:
mid (
(Upper_Seq (C,n)),2,
(len (Upper_Seq (C,n))))
is_in_the_area_of Cage (
C,
n)
by A126, JORDAN1E:17, SPRECT_2:22;
(Upper_Seq (C,n)) /. (len (Upper_Seq (C,n))) = E-max (L~ (Cage (C,n)))
by JORDAN1F:7;
then
((Upper_Seq (C,n)) /. (len (Upper_Seq (C,n)))) `1 = E-bound (L~ (Cage (C,n)))
by EUCLID:52;
then A129:
((mid ((Upper_Seq (C,n)),2,(len (Upper_Seq (C,n))))) /. (len (mid ((Upper_Seq (C,n)),2,(len (Upper_Seq (C,n))))))) `1 = E-bound (L~ (Cage (C,n)))
by A126, A127, SPRECT_2:9;
((Upper_Seq (C,n)) /. (1 + 1)) `1 = W-bound (L~ (Cage (C,n)))
by JORDAN1G:31;
then
((mid ((Upper_Seq (C,n)),2,(len (Upper_Seq (C,n))))) /. 1) `1 = W-bound (L~ (Cage (C,n)))
by A126, A127, SPRECT_2:8;
then A130:
mid (
(Upper_Seq (C,n)),2,
(len (Upper_Seq (C,n))))
is_a_h.c._for Cage (
C,
n)
by A128, A129, SPRECT_2:def 2;
now for m being Nat st m in dom <*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> holds
( W-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `1 & (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `1 <= E-bound (L~ (Cage (C,n))) & S-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `2 & (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `2 <= N-bound (L~ (Cage (C,n))) )let m be
Nat;
( m in dom <*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> implies ( W-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `1 & (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `1 <= E-bound (L~ (Cage (C,n))) & S-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `2 & (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `2 <= N-bound (L~ (Cage (C,n))) ) )assume A131:
m in dom <*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*>
;
( W-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `1 & (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `1 <= E-bound (L~ (Cage (C,n))) & S-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `2 & (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `2 <= N-bound (L~ (Cage (C,n))) )then
m in Seg 1
by FINSEQ_1:38;
then
m = 1
by FINSEQ_1:2, TARSKI:def 1;
then
<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> . m = (Gauge (C,n)) * (
i,
(width (Gauge (C,n))))
by FINSEQ_1:40;
then A132:
<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m = (Gauge (C,n)) * (
i,
(width (Gauge (C,n))))
by A131, PARTFUN1:def 6;
((Gauge (C,n)) * (1,(width (Gauge (C,n))))) `1 <= ((Gauge (C,n)) * (i,(width (Gauge (C,n))))) `1
by A1, A2, A13, SPRECT_3:13;
hence
W-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `1
by A12, A13, A132, JORDAN1A:73;
( (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `1 <= E-bound (L~ (Cage (C,n))) & S-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `2 & (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `2 <= N-bound (L~ (Cage (C,n))) )
((Gauge (C,n)) * (i,(width (Gauge (C,n))))) `1 <= ((Gauge (C,n)) * ((len (Gauge (C,n))),(width (Gauge (C,n))))) `1
by A1, A2, A13, SPRECT_3:13;
hence
(<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `1 <= E-bound (L~ (Cage (C,n)))
by A12, A13, A132, JORDAN1A:71;
( S-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `2 & (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `2 <= N-bound (L~ (Cage (C,n))) )
(<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `2 = N-bound (L~ (Cage (C,n)))
by A1, A2, A12, A132, JORDAN1A:70;
hence
S-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `2
by SPRECT_1:22;
(<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `2 <= N-bound (L~ (Cage (C,n)))thus
(<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `2 <= N-bound (L~ (Cage (C,n)))
by A1, A2, A12, A132, JORDAN1A:70;
verum end; then A133:
<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> is_in_the_area_of Cage (
C,
n)
by SPRECT_2:def 1;
<*((Gauge (C,n)) * (i,j))*> is_in_the_area_of Cage (
C,
n)
by A104, JORDAN1E:18, SPRECT_3:46;
then
L_Cut (
(Lower_Seq (C,n)),
((Gauge (C,n)) * (i,j)))
is_in_the_area_of Cage (
C,
n)
by A104, JORDAN1E:18, SPRECT_3:56;
then
<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) is_in_the_area_of Cage (
C,
n)
by A133, SPRECT_2:24;
then A134:
Rev (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) is_in_the_area_of Cage (
C,
n)
by SPRECT_3:51;
(<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) /. 1
= (Gauge (C,n)) * (
i,
(width (Gauge (C,n))))
by FINSEQ_5:15;
then
((<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) /. 1) `2 = N-bound (L~ (Cage (C,n)))
by A1, A2, A12, JORDAN1A:70;
then
((Rev (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))))) /. (len (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))))) `2 = N-bound (L~ (Cage (C,n)))
by FINSEQ_5:65;
then A135:
((Rev (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))))) /. (len (Rev (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))))))) `2 = N-bound (L~ (Cage (C,n)))
by FINSEQ_5:def 3;
((<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) /. (len (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))))) `2 = S-bound (L~ (Cage (C,n)))
by A104, A110, EUCLID:52;
then
((Rev (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))))) /. 1) `2 = S-bound (L~ (Cage (C,n)))
by FINSEQ_5:65;
then
Rev (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) is_a_v.c._for Cage (
C,
n)
by A134, A135, SPRECT_2:def 3;
then
L~ (mid ((Upper_Seq (C,n)),2,(len (Upper_Seq (C,n))))) meets L~ (Rev (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))))
by A112, A120, A121, A124, A125, A130, SPRECT_2:29;
then
L~ (mid ((Upper_Seq (C,n)),2,(len (Upper_Seq (C,n))))) meets L~ (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))))
by SPPOL_2:22;
then consider x being
object such that A136:
x in L~ (mid ((Upper_Seq (C,n)),2,(len (Upper_Seq (C,n)))))
and A137:
x in L~ (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))))
by XBOOLE_0:3;
A138:
L~ (mid ((Upper_Seq (C,n)),2,(len (Upper_Seq (C,n))))) c= L~ (Upper_Seq (C,n))
by A9, A10, JORDAN4:35;
A139:
L~ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) c= L~ (Lower_Seq (C,n))
by A104, JORDAN3:42;
A140:
L~ (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) = (LSeg (((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) /. 1))) \/ (L~ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))))
by A105, SPPOL_2:20;
(Upper_Seq (C,n)) /. 1
= W-min (L~ (Cage (C,n)))
by JORDAN1F:5;
then A141:
not
W-min (L~ (Cage (C,n))) in L~ (mid ((Upper_Seq (C,n)),2,(len (Upper_Seq (C,n)))))
by A123, JORDAN5B:16;
now L~ (Upper_Seq (C,n)) meets L~ <*((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))*>per cases
( x in LSeg (((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) /. 1)) or x in L~ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) )
by A137, A140, XBOOLE_0:def 3;
suppose
x in LSeg (
((Gauge (C,n)) * (i,(width (Gauge (C,n))))),
((L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) /. 1))
;
L~ (Upper_Seq (C,n)) meets L~ <*((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))*>then
x in L~ <*((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))*>
by A111, SPPOL_2:21;
hence
L~ (Upper_Seq (C,n)) meets L~ <*((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))*>
by A136, A138, XBOOLE_0:3;
verum end; suppose A142:
x in L~ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))
;
L~ (Upper_Seq (C,n)) meets L~ <*((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))*>then
x in (L~ (Lower_Seq (C,n))) /\ (L~ (Upper_Seq (C,n)))
by A136, A138, A139, XBOOLE_0:def 4;
then
x in {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))}
by JORDAN1E:16;
then A143:
x = E-max (L~ (Cage (C,n)))
by A136, A141, TARSKI:def 2;
1
in dom (Lower_Seq (C,n))
by A11, FINSEQ_3:25;
then (Lower_Seq (C,n)) . 1 =
(Lower_Seq (C,n)) /. 1
by PARTFUN1:def 6
.=
E-max (L~ (Cage (C,n)))
by JORDAN1F:6
;
then
x = (Gauge (C,n)) * (
i,
j)
by A104, A142, A143, JORDAN1E:7;
then
x in LSeg (
((Gauge (C,n)) * (i,(width (Gauge (C,n))))),
((Gauge (C,n)) * (i,j)))
by RLTOPSP1:68;
then
x in L~ <*((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))*>
by SPPOL_2:21;
hence
L~ (Upper_Seq (C,n)) meets L~ <*((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))*>
by A136, A138, XBOOLE_0:3;
verum end; end; end; then
L~ <*((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))*> meets L~ (Upper_Seq (C,n))
;
hence
LSeg (
((Gauge (C,n)) * (i,(width (Gauge (C,n))))),
((Gauge (C,n)) * (i,j)))
meets L~ (Upper_Seq (C,n))
by SPPOL_2:21;
verum end; suppose A144:
(Gauge (C,n)) * (
i,
j)
in L~ (Upper_Seq (C,n))
;
LSeg (((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))) meets L~ (Upper_Seq (C,n))
(Gauge (C,n)) * (
i,
j)
in LSeg (
((Gauge (C,n)) * (i,(width (Gauge (C,n))))),
((Gauge (C,n)) * (i,j)))
by RLTOPSP1:68;
hence
LSeg (
((Gauge (C,n)) * (i,(width (Gauge (C,n))))),
((Gauge (C,n)) * (i,j)))
meets L~ (Upper_Seq (C,n))
by A144, XBOOLE_0:3;
verum end; suppose A145:
(
(Gauge (C,n)) * (
i,
j)
in L~ (Lower_Seq (C,n)) &
(Gauge (C,n)) * (
i,
j)
= (Lower_Seq (C,n)) . (len (Lower_Seq (C,n))) )
;
LSeg (((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))) meets L~ (Upper_Seq (C,n))
len (Lower_Seq (C,n)) in dom (Lower_Seq (C,n))
by A11, FINSEQ_3:25;
then A146:
(Lower_Seq (C,n)) . (len (Lower_Seq (C,n))) =
(Lower_Seq (C,n)) /. (len (Lower_Seq (C,n)))
by PARTFUN1:def 6
.=
W-min (L~ (Cage (C,n)))
by JORDAN1F:8
;
A147:
rng (Upper_Seq (C,n)) c= L~ (Upper_Seq (C,n))
by A7, SPPOL_2:18, XXREAL_0:2;
A148:
W-min (L~ (Cage (C,n))) in rng (Upper_Seq (C,n))
by JORDAN1J:5;
(Gauge (C,n)) * (
i,
j)
in LSeg (
((Gauge (C,n)) * (i,(width (Gauge (C,n))))),
((Gauge (C,n)) * (i,j)))
by RLTOPSP1:68;
hence
LSeg (
((Gauge (C,n)) * (i,(width (Gauge (C,n))))),
((Gauge (C,n)) * (i,j)))
meets L~ (Upper_Seq (C,n))
by A145, A146, A147, A148, XBOOLE_0:3;
verum end; end; end;
hence
LSeg (((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))) meets L~ (Upper_Seq (C,n))
; verum