let n be Nat; :: thesis: 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); :: thesis: 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; :: 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: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)));

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

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

end;

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: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; :: thesis: verum

end;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; :: thesis: verum

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: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))

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))));

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;

<*((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;

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

end;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; :: thesis: verum

now :: thesis: not SW-corner (L~ (Cage (C,n))) in rng (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))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;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) )
;

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))) = <*((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))

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; :: thesis: verum

end;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

then A65:
not SW-corner (L~ (Cage (C,n))) in {((Gauge (C,n)) * (i,j))}
by A5, TARSKI:def 1;
assume
SW-corner (L~ (Cage (C,n))) in L~ (Cage (C,n))
; :: thesis: 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;

end;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;

end;

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: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; :: thesis: verum

end;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; :: thesis: verum

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: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; :: thesis: verum

end;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; :: thesis: verum

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; :: thesis: verum

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 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; :: thesis: verum

end;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; :: thesis: verum

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 :: thesis: not (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in rng (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))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;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) )
;

end;

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: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; :: thesis: verum

end;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; :: thesis: verum

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 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; :: thesis: verum

end;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; :: thesis: verum

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 :: thesis: 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))) )

then A91:
<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> is_in_the_area_of Cage (C,n)
by SPRECT_2:def 1;( 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; :: 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 A89: 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: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; :: 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:13;

hence (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `1 <= E-bound (L~ (Cage (C,n))) by A12, A13, A90, JORDAN1A:71; :: 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, A90, JORDAN1A:70;

hence S-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `2 by SPRECT_1:22; :: 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, A90, JORDAN1A:70; :: thesis: verum

end;assume A89: 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: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; :: 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:13;

hence (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `1 <= E-bound (L~ (Cage (C,n))) by A12, A13, A90, JORDAN1A:71; :: 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, A90, JORDAN1A:70;

hence S-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `2 by SPRECT_1:22; :: 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, A90, JORDAN1A:70; :: thesis: verum

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

then
L~ <*((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))*> meets L~ (Upper_Seq (C,n))
;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;

end;

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

end;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; :: thesis: verum

suppose A101:
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 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; :: thesis: verum

end;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; :: thesis: verum

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)))))
; :: 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, 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; :: thesis: verum

end;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; :: thesis: verum

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

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)) )
; :: thesis: 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))));

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;

<*((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;

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;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 :: thesis: not (Gauge (C,n)) * (i,(width (Gauge (C,n)))) in rng (L_Cut ((Lower_Seq (C,n)),((Gauge (C,n)) * (i,j))))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;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) )
;

end;

suppose A116:
(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: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; :: thesis: verum

end;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; :: thesis: verum

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 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; :: thesis: verum

end;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; :: thesis: verum

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 :: thesis: 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))) )

then A133:
<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> is_in_the_area_of Cage (C,n)
by SPRECT_2:def 1;( 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; :: 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 A131: 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: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; :: 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:13;

hence (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `1 <= E-bound (L~ (Cage (C,n))) by A12, A13, A132, JORDAN1A:71; :: 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, A132, JORDAN1A:70;

hence S-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `2 by SPRECT_1:22; :: 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, A132, JORDAN1A:70; :: thesis: verum

end;assume A131: 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: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; :: 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:13;

hence (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `1 <= E-bound (L~ (Cage (C,n))) by A12, A13, A132, JORDAN1A:71; :: 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, A132, JORDAN1A:70;

hence S-bound (L~ (Cage (C,n))) <= (<*((Gauge (C,n)) * (i,(width (Gauge (C,n)))))*> /. m) `2 by SPRECT_1:22; :: 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, A132, JORDAN1A:70; :: thesis: verum

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

then
L~ <*((Gauge (C,n)) * (i,(width (Gauge (C,n))))),((Gauge (C,n)) * (i,j))*> meets L~ (Upper_Seq (C,n))
;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;

end;

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 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; :: thesis: verum

end;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; :: thesis: verum

suppose A142:
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 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; :: thesis: verum

end;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; :: thesis: verum

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

suppose A144:
(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: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; :: thesis: verum

end;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; :: thesis: verum

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

end;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; :: thesis: verum