let n be Element of NAT ; :: thesis: for C being connected compact non horizontal non vertical Subset of (TOP-REAL 2)
for i, j being Element of 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); :: thesis: for i, j being Element of 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 Element of NAT ; :: thesis: ( 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)) ; :: thesis: 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:17;
A7: len (Upper_Seq (C,n)) >= 3 by JORDAN1E:19;
A8: len (Lower_Seq (C,n)) >= 3 by JORDAN1E:19;
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:13;
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:91;
set Ema = E-max (L~ (Cage (C,n)));

now

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)) ) ; :: thesis: 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:92;
A17: (E-max (L~ (Cage (C,n)))) `1 = E-bound (L~ (Cage (C,n))) by EUCLID:56;
A18: N-bound (L~ (Cage (C,n))) = ((Gauge (C,n)) * ((len (Gauge (C,n))),(width (Gauge (C,n))))) `2 by A1, A12, A15, JORDAN1A:91;
E-max (L~ (Cage (C,n))) in L~ (Cage (C,n)) by SPRECT_1:16;
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:71;
A20: ((Gauge (C,n)) * (i,j)) `1 = E-bound (L~ (Cage (C,n))) by A3, A4, A12, A15, JORDAN1A:92;
then (Gauge (C,n)) * (i,j) in E-most (L~ (Cage (C,n))) by A5, SPRECT_2:17;
then (E-max (L~ (Cage (C,n)))) `2 >= ((Gauge (C,n)) * (i,j)) `2 by PSCOMP_1:108;
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:8;
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 REVROT_1:3;
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; :: thesis: 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)) ) ; :: thesis: 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:7;
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:27;
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:27;
A28: len (Lower_Seq (C,n)) in dom (Lower_Seq (C,n)) by A11, FINSEQ_3:27;
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 8
.= (Lower_Seq (C,n)) . (len (Lower_Seq (C,n))) by A23, JORDAN1B:5
.= (Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) by A28, PARTFUN1:def 8
.= 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:11;
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 8
.= (Gauge (C,n)) * (i,j) by A23, JORDAN3:58 ;
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:8;
A33: 1 + (len (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) >= 1 + 1 by A25, XREAL_1:9;
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:19
.= (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:34;
then SW-corner (L~ (Cage (C,n))) <> (Gauge (C,n)) * (i,(width (Gauge (C,n)))) by A14, EUCLID:56;
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:56;
len (Cage (C,n)) > 4 by GOBOARD7:36;
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)) ; :: thesis: contradiction
A39: (SW-corner (L~ (Cage (C,n)))) `1 = W-bound (L~ (Cage (C,n))) by EUCLID:56;
A40: (SW-corner (L~ (Cage (C,n)))) `2 = S-bound (L~ (Cage (C,n))) by EUCLID:56;
then (SW-corner (L~ (Cage (C,n)))) `2 <= N-bound (L~ (Cage (C,n))) by SPRECT_1:24;
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:28;
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:88;
(W-min (L~ (Cage (C,n)))) `2 >= (SW-corner (L~ (Cage (C,n)))) `2 by PSCOMP_1:87;
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:85;
hence contradiction by A23, A42, TOPREAL3:11; :: thesis: verum

end;

now

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) ; :: thesis: 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 4;
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:44;
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:55;
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)) ; :: thesis: contradiction
then consider i being Element of 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 7;

suppose A47: ((Cage (C,n)) /. i) `1 = ((Cage (C,n)) /. (i + 1)) `1 ; :: thesis: contradiction

then 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:56;
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:13;
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:13;
A54: i in dom (Cage (C,n)) by A44, A50, FINSEQ_3:27;
A55: i + 1 in dom (Cage (C,n)) by A45, A52, FINSEQ_3:27;
( ((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:10;
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:11;
hence contradiction by A37, A54, A55, PARTFUN2:4; :: thesis: verum

end;

suppose A56: ((Cage (C,n)) /. i) `2 = ((Cage (C,n)) /. (i + 1)) `2 ; :: thesis: contradiction

then 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:56;
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:14;
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:14;
A63: i in dom (Cage (C,n)) by A44, A59, FINSEQ_3:27;
A64: i + 1 in dom (Cage (C,n)) by A45, A61, FINSEQ_3:27;
( ((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:9;
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:11;
hence contradiction by A37, A63, A64, PARTFUN2:4; :: thesis: 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:125;
rng (Lower_Seq (C,n)) c= rng (Cage (C,n)) by JORDAN1G:47;
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, XBOOLE_1:1;
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; :: thesis: verum

end;

suppose (Gauge (C,n)) * (i,j) = (Lower_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1) ; :: thesis: 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 4;
then A67: rng (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) c= rng (Lower_Seq (C,n)) by FINSEQ_6:125;
rng (Lower_Seq (C,n)) c= rng (Cage (C,n)) by JORDAN1G:47;
then rng (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) c= rng (Cage (C,n)) by A67, XBOOLE_1:1;
hence not SW-corner (L~ (Cage (C,n))) in rng (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) by A37; :: thesis: 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:44;
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:56;
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:55;
A69: not (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in L~ (Lower_Seq (C,n)) by A1, A23, JORDAN1G:53;
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:53;
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:55;
set ci = mid ((Lower_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1),(len (Lower_Seq (C,n))));

now

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) ; :: thesis: 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:125;
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:44;
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 4; :: thesis: verum

end;

suppose (Gauge (C,n)) * (i,j) = (Lower_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1) ; :: thesis: 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 4;
then rng (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) c= rng (Lower_Seq (C,n)) by FINSEQ_6:125;
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; :: thesis: 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:56;
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:55;
A74: <*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> is one-to-one by FINSEQ_3:102;
A75: L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))) is being_S-Seq by A23, JORDAN3:69;
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:98;
<*(SW-corner (L~ (Cage (C,n))))*> is one-to-one by FINSEQ_3:102;
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:98;
A78: <*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> is special ;
(<*((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:56
.= ((Gauge (C,n)) * (i,(width (Gauge (C,n))))) `1 by FINSEQ_4:25
.= ((Gauge (C,n)) * (i,1)) `1 by A1, A2, A13, GOBOARD5:3
.= ((L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) /. 1) `1 by A1, A2, A3, A4, A31, GOBOARD5:3 ;
then A79: <*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) is special by A75, GOBOARD2:13;
A80: <*(SW-corner (L~ (Cage (C,n))))*> is special ;
((<*((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:85
.= (<*(SW-corner (L~ (Cage (C,n))))*> /. 1) `1 by FINSEQ_4:25 ;
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 A79, GOBOARD2:13;
then A81: 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:42;
A82: len (Upper_Seq (C,n)) >= 2 + 1 by JORDAN1E:19;
then A83: len (Upper_Seq (C,n)) > 2 by NAT_1:13;
len (Upper_Seq (C,n)) > 1 by A82, XXREAL_0:2;
then A84: mid ((Upper_Seq (C,n)),2,(len (Upper_Seq (C,n)))) is S-Sequence_in_R2 by A83, JORDAN3:39;
then A85: 2 <= len (mid ((Upper_Seq (C,n)),2,(len (Upper_Seq (C,n))))) by TOPREAL1:def 10;
3 <= len (Upper_Seq (C,n)) by JORDAN1E:19;
then 2 <= len (Upper_Seq (C,n)) by XXREAL_0:2;
then A86: 2 in dom (Upper_Seq (C,n)) by FINSEQ_3:27;
A87: len (Upper_Seq (C,n)) in dom (Upper_Seq (C,n)) by FINSEQ_5:6;
then A88: mid ((Upper_Seq (C,n)),2,(len (Upper_Seq (C,n)))) is_in_the_area_of Cage (C,n) by A86, JORDAN1E:21, SPRECT_2:26;
(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:56;
then A89: ((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 A86, A87, SPRECT_2:13;
((Upper_Seq (C,n)) /. (1 + 1)) `1 = W-bound (L~ (Cage (C,n))) by JORDAN1G:39;
then ((mid ((Upper_Seq (C,n)),2,(len (Upper_Seq (C,n))))) /. 1) `1 = W-bound (L~ (Cage (C,n))) by A86, A87, SPRECT_2:12;
then A90: mid ((Upper_Seq (C,n)),2,(len (Upper_Seq (C,n)))) is_a_h.c._for Cage (C,n) by A88, A89, SPRECT_2:def 2;

now

let m be Element of NAT ; :: thesis: ( 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 A91: m in dom <*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ; :: thesis: ( 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:55;
then m = 1 by FINSEQ_1:4, TARSKI:def 1;
then <*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> . m = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) by FINSEQ_1:57;
then A92: <*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) by A91, PARTFUN1:def 8;
((Gauge (C,n)) * (1,(width (Gauge (C,n))))) `1 <= ((Gauge (C,n)) * (i,(width (Gauge (C,n))))) `1 by A1, A2, A13, SPRECT_3:25;
hence W-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `1 by A12, A13, A92, JORDAN1A:94; :: thesis: ( (<*((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:25;
hence (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `1 <= E-bound (L~ (Cage (C,n))) by A12, A13, A92, JORDAN1A:92; :: thesis: ( 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, A92, JORDAN1A:91;
hence S-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `2 by SPRECT_1:24; :: thesis: (<*((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, A92, JORDAN1A:91; :: thesis: verum

end;

then A93: <*((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:22, SPRECT_3:63;
then L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))) is_in_the_area_of Cage (C,n) by A23, JORDAN1E:22, SPRECT_3:73;
then A94: <*((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 A93, SPRECT_2:28;
<*(SW-corner (L~ (Cage (C,n))))*> is_in_the_area_of Cage (C,n) by SPRECT_2: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))))*> is_in_the_area_of Cage (C,n) by A94, SPRECT_2:28;
then A95: 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:68;
(<*((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:45;
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: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))))*>) /. 1) `2 = N-bound (L~ (Cage (C,n))) by A1, A2, A12, JORDAN1A:91;
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:68;
then A96: ((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:19;
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:82;
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:56;
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:68;
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 A95, A96, 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, A81, A84, A85, A90, SPRECT_2:33;
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 set such that
A97: x in L~ (mid ((Upper_Seq (C,n)),2,(len (Upper_Seq (C,n))))) and
A98: 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;
A99: L~ (mid ((Upper_Seq (C,n)),2,(len (Upper_Seq (C,n))))) c= L~ (Upper_Seq (C,n)) by A9, A10, JORDAN4:47;
A100: L~ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) c= L~ (Lower_Seq (C,n)) by A23, JORDAN3:77;
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:45
.= (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 A101: ( 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 A98, XBOOLE_0:def 3;
(Upper_Seq (C,n)) /. 1 = W-min (L~ (Cage (C,n))) by JORDAN1F:5;
then A102: not W-min (L~ (Cage (C,n))) in L~ (mid ((Upper_Seq (C,n)),2,(len (Upper_Seq (C,n))))) by A83, JORDAN5B:16;

now

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 A101, 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)) ; :: thesis: 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 A97, A99, XBOOLE_0:3; :: thesis: verum

end;

suppose A103: x in L~ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) ; :: thesis: 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 A97, A99, A100, XBOOLE_0:def 4;
then x in {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} by JORDAN1E:20;
then A104: x = E-max (L~ (Cage (C,n))) by A97, A102, TARSKI:def 2;
1 in dom (Lower_Seq (C,n)) by A11, FINSEQ_3:27;
then (Lower_Seq (C,n)) . 1 = (Lower_Seq (C,n)) /. 1 by PARTFUN1:def 8
.= E-max (L~ (Cage (C,n))) by JORDAN1F:6 ;
then x = (Gauge (C,n)) * (i,j) by A23, A103, A104, JORDAN1E:11;
then x in LSeg (((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))) by RLTOPSP1:69;
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 A97, A99, XBOOLE_0:3; :: thesis: verum

end;

suppose A105: 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))))) ; :: thesis: 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, A97, A99, 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, A105, XBOOLE_0:def 4;
then x in {(W-min (L~ (Cage (C,n))))} by PSCOMP_1:92;
hence L~ (Upper_Seq (C,n)) meets L~ <*((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))*> by A97, A102, TARSKI:def 1; :: thesis: 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; :: thesis: verum

end;

suppose A106: ( (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)) ) ; :: thesis: LSeg (((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))) meets L~ (Upper_Seq (C,n))

then A107: not L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))) is empty by JORDAN1E:7;
then A108: 0 + 1 <= len (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) by NAT_1:13;
then A109: 1 in dom (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) by FINSEQ_3:27;
set v = <*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))));
A110: 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 A108, FINSEQ_3:27;
A111: len (Lower_Seq (C,n)) in dom (Lower_Seq (C,n)) by A11, FINSEQ_3:27;
(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 A110, PARTFUN1:def 8
.= (Lower_Seq (C,n)) . (len (Lower_Seq (C,n))) by A106, JORDAN1B:5
.= (Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) by A111, PARTFUN1:def 8
.= W-min (L~ (Cage (C,n))) by JORDAN1F:8 ;
then A112: (<*((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 A107, SPRECT_3:11;
A113: (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 A109, PARTFUN1:def 8
.= (Gauge (C,n)) * (i,j) by A106, JORDAN3:58 ;
1 + (len (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))) >= 1 + 1 by A108, XREAL_1:9;
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 A114: 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;
A115: not (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in L~ (Lower_Seq (C,n)) by A1, A106, JORDAN1G:53;
rng (Lower_Seq (C,n)) c= L~ (Lower_Seq (C,n)) by A8, SPPOL_2:18, XXREAL_0:2;
then A116: not (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in rng (Lower_Seq (C,n)) by A1, A106, JORDAN1G:53;
not (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in {((Gauge (C,n)) * (i,j))} by A106, A115, TARSKI:def 1;
then A117: not (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in rng <*((Gauge (C,n)) * (i,j))*> by FINSEQ_1:55;
set ci = mid ((Lower_Seq (C,n)),((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1),(len (Lower_Seq (C,n))));

now

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 A118: (Gauge (C,n)) * (i,j) <> (Lower_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1) ; :: thesis: 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:125;
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 A116;
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 A117, 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:44;
hence not (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in rng (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) by A118, JORDAN3:def 4; :: thesis: verum

end;

suppose (Gauge (C,n)) * (i,j) = (Lower_Seq (C,n)) . ((Index (((Gauge (C,n)) * (i,j)),(Lower_Seq (C,n)))) + 1) ; :: thesis: 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 4;
then rng (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) c= rng (Lower_Seq (C,n)) by FINSEQ_6:125;
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; :: thesis: 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:56;
then A119: 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:55;
A120: <*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> is one-to-one by FINSEQ_3:102;
A121: L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))) is being_S-Seq by A106, JORDAN3:69;
then A122: <*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) is one-to-one by A119, A120, FINSEQ_3:98;
A123: <*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> is special ;
(<*((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:56
.= ((Gauge (C,n)) * (i,(width (Gauge (C,n))))) `1 by FINSEQ_4:25
.= ((Gauge (C,n)) * (i,1)) `1 by A1, A2, A13, GOBOARD5:3
.= ((L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) /. 1) `1 by A1, A2, A3, A4, A113, GOBOARD5:3 ;
then <*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ^ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) is special by A121, GOBOARD2:13;
then A124: 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:42;
A125: len (Upper_Seq (C,n)) >= 2 + 1 by JORDAN1E:19;
then A126: len (Upper_Seq (C,n)) > 2 by NAT_1:13;
len (Upper_Seq (C,n)) > 1 by A125, XXREAL_0:2;
then A127: mid ((Upper_Seq (C,n)),2,(len (Upper_Seq (C,n)))) is S-Sequence_in_R2 by A126, JORDAN3:39;
then A128: 2 <= len (mid ((Upper_Seq (C,n)),2,(len (Upper_Seq (C,n))))) by TOPREAL1:def 10;
3 <= len (Upper_Seq (C,n)) by JORDAN1E:19;
then 2 <= len (Upper_Seq (C,n)) by XXREAL_0:2;
then A129: 2 in dom (Upper_Seq (C,n)) by FINSEQ_3:27;
A130: len (Upper_Seq (C,n)) in dom (Upper_Seq (C,n)) by FINSEQ_5:6;
then A131: mid ((Upper_Seq (C,n)),2,(len (Upper_Seq (C,n)))) is_in_the_area_of Cage (C,n) by A129, JORDAN1E:21, SPRECT_2:26;
(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:56;
then A132: ((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 A129, A130, SPRECT_2:13;
((Upper_Seq (C,n)) /. (1 + 1)) `1 = W-bound (L~ (Cage (C,n))) by JORDAN1G:39;
then ((mid ((Upper_Seq (C,n)),2,(len (Upper_Seq (C,n))))) /. 1) `1 = W-bound (L~ (Cage (C,n))) by A129, A130, SPRECT_2:12;
then A133: mid ((Upper_Seq (C,n)),2,(len (Upper_Seq (C,n)))) is_a_h.c._for Cage (C,n) by A131, A132, SPRECT_2:def 2;

now

let m be Element of NAT ; :: thesis: ( 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 A134: m in dom <*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> ; :: thesis: ( 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:55;
then m = 1 by FINSEQ_1:4, TARSKI:def 1;
then <*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> . m = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) by FINSEQ_1:57;
then A135: <*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m = (Gauge (C,n)) * (i,(width (Gauge (C,n)))) by A134, PARTFUN1:def 8;
((Gauge (C,n)) * (1,(width (Gauge (C,n))))) `1 <= ((Gauge (C,n)) * (i,(width (Gauge (C,n))))) `1 by A1, A2, A13, SPRECT_3:25;
hence W-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `1 by A12, A13, A135, JORDAN1A:94; :: thesis: ( (<*((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:25;
hence (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `1 <= E-bound (L~ (Cage (C,n))) by A12, A13, A135, JORDAN1A:92; :: thesis: ( 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, A135, JORDAN1A:91;
hence S-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `2 by SPRECT_1:24; :: thesis: (<*((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, A135, JORDAN1A:91; :: thesis: verum

end;

then A136: <*((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 A106, JORDAN1E:22, SPRECT_3:63;
then L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))) is_in_the_area_of Cage (C,n) by A106, JORDAN1E:22, SPRECT_3:73;
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 A136, SPRECT_2:28;
then A137: 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:68;
(<*((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:16;
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:91;
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:68;
then A138: ((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 A106, A112, EUCLID:56;
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:68;
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 A137, A138, 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 A114, A122, A124, A127, A128, A133, SPRECT_2:33;
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 set such that
A139: x in L~ (mid ((Upper_Seq (C,n)),2,(len (Upper_Seq (C,n))))) and
A140: 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;
A141: L~ (mid ((Upper_Seq (C,n)),2,(len (Upper_Seq (C,n))))) c= L~ (Upper_Seq (C,n)) by A9, A10, JORDAN4:47;
A142: L~ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) c= L~ (Lower_Seq (C,n)) by A106, JORDAN3:77;
A143: 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 A107, SPPOL_2:20;
(Upper_Seq (C,n)) /. 1 = W-min (L~ (Cage (C,n))) by JORDAN1F:5;
then A144: not W-min (L~ (Cage (C,n))) in L~ (mid ((Upper_Seq (C,n)),2,(len (Upper_Seq (C,n))))) by A126, JORDAN5B:16;

now

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 A140, A143, 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)) ; :: thesis: 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 A113, 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 A139, A141, XBOOLE_0:3; :: thesis: verum

end;

suppose A145: x in L~ (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j)))) ; :: thesis: 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 A139, A141, A142, XBOOLE_0:def 4;
then x in {(W-min (L~ (Cage (C,n)))),(E-max (L~ (Cage (C,n))))} by JORDAN1E:20;
then A146: x = E-max (L~ (Cage (C,n))) by A139, A144, TARSKI:def 2;
1 in dom (Lower_Seq (C,n)) by A11, FINSEQ_3:27;
then (Lower_Seq (C,n)) . 1 = (Lower_Seq (C,n)) /. 1 by PARTFUN1:def 8
.= E-max (L~ (Cage (C,n))) by JORDAN1F:6 ;
then x = (Gauge (C,n)) * (i,j) by A106, A145, A146, JORDAN1E:11;
then x in LSeg (((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))) by RLTOPSP1:69;
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 A139, A141, XBOOLE_0:3; :: thesis: 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; :: thesis: verum

end;

suppose A147: (Gauge (C,n)) * (i,j) in L~ (Upper_Seq (C,n)) ; :: thesis: 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:69;
hence LSeg (((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))) meets L~ (Upper_Seq (C,n)) by A147, XBOOLE_0:3; :: thesis: verum

end;

suppose A148: ( (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))) ) ; :: thesis: 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:27;
then A149: (Lower_Seq (C,n)) . (len (Lower_Seq (C,n))) = (Lower_Seq (C,n)) /. (len (Lower_Seq (C,n))) by PARTFUN1:def 8
.= W-min (L~ (Cage (C,n))) by JORDAN1F:8 ;
A150: rng (Upper_Seq (C,n)) c= L~ (Upper_Seq (C,n)) by A7, SPPOL_2:18, XXREAL_0:2;
A151: 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:69;
hence LSeg (((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))) meets L~ (Upper_Seq (C,n)) by A148, A149, A150, A151, XBOOLE_0:3; :: thesis: 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)) ; :: thesis: verum