let D be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: not LeftComp (SpStSeq D) is Bounded
set f = SpStSeq D;
consider q3 being Element of LeftComp (SpStSeq D);
reconsider q4 = q3 as Point of (TOP-REAL 2) ;
set r1 = |.((1 / 2) * (((SpStSeq D) /. 1) + ((SpStSeq D) /. 2))).|;
reconsider f1 = SpStSeq D as non constant standard special_circular_sequence ;
A1: W-bound (L~ f1) < E-bound (L~ f1) by SPRECT_1:33;
A2: (N-min (L~ f1)) `2 = N-bound (L~ f1) by EUCLID:56;
then ((N-min (L~ f1)) `2 ) + ((N-max (L~ f1)) `2 ) = (N-bound (L~ f1)) + (N-bound (L~ f1)) by EUCLID:56
.= 2 * (N-bound (L~ (SpStSeq D))) ;
then A3: (1 / 2) * (((N-min (L~ (SpStSeq D))) `2 ) + ((N-max (L~ (SpStSeq D))) `2 )) = N-bound (L~ (SpStSeq D)) ;
A4: len f1 = 5 by SPRECT_1:90;
then 5 in Seg (len f1) by FINSEQ_1:3;
then A5: 5 in dom f1 by FINSEQ_1:def 3;
then 5 in dom (Y_axis f1) by SPRECT_2:20;
then A6: (Y_axis f1) . 5 = (f1 /. 5) `2 by GOBOARD1:def 4;
4 in Seg (len f1) by A4, FINSEQ_1:3;
then A7: 4 in dom f1 by FINSEQ_1:def 3;
then 4 in dom (Y_axis f1) by SPRECT_2:20;
then ( f1 /. 4 = S-min (L~ f1) & (Y_axis f1) . 4 = (f1 /. 4) `2 ) by GOBOARD1:def 4, SPRECT_1:94;
then A8: (Y_axis f1) . 4 = S-bound (L~ f1) by EUCLID:56;
3 in Seg (len f1) by A4, FINSEQ_1:3;
then A9: 3 in dom f1 by FINSEQ_1:def 3;
then 3 in dom (Y_axis f1) by SPRECT_2:20;
then ( f1 /. 3 = S-max (L~ f1) & (Y_axis f1) . 3 = (f1 /. 3) `2 ) by GOBOARD1:def 4, SPRECT_1:93;
then A10: (Y_axis f1) . 3 = S-bound (L~ f1) by EUCLID:56;
3 in dom (X_axis f1) by A9, SPRECT_2:19;
then ( f1 /. 3 = E-min (L~ f1) & (X_axis f1) . 3 = (f1 /. 3) `1 ) by GOBOARD1:def 3, SPRECT_1:93;
then A11: (X_axis f1) . 3 = E-bound (L~ f1) by EUCLID:56;
5 in dom (X_axis f1) by A5, SPRECT_2:19;
then A12: (X_axis f1) . 5 = (f1 /. 5) `1 by GOBOARD1:def 3;
assume LeftComp (SpStSeq D) is Bounded ; :: thesis: contradiction
then consider r being Real such that
A13: for q being Point of (TOP-REAL 2) st q in LeftComp (SpStSeq D) holds
|.q.| < r by Th40;
set q1 = |[0 ,((|.((1 / 2) * (((SpStSeq D) /. 1) + ((SpStSeq D) /. 2))).| + r) + 1)]| + ((1 / 2) * (((SpStSeq D) /. 1) + ((SpStSeq D) /. 2)));
A14: f1 /. 1 = N-min (L~ f1) by SPRECT_1:91;
4 in dom (X_axis f1) by A7, SPRECT_2:19;
then ( f1 /. 4 = W-min (L~ f1) & (X_axis f1) . 4 = (f1 /. 4) `1 ) by GOBOARD1:def 3, SPRECT_1:94;
then A15: (X_axis f1) . 4 = W-bound (L~ f1) by EUCLID:56;
A16: GoB f1 = GoB (Incr (X_axis f1)),(Incr (Y_axis f1)) by GOBOARD2:def 3;
A17: f1 /. 2 = E-max (L~ f1) by SPRECT_1:92;
2 in Seg (len f1) by A4, FINSEQ_1:3;
then A18: 2 in dom f1 by FINSEQ_1:def 3;
then A19: 2 in dom (X_axis f1) by SPRECT_2:19;
then (X_axis f1) . 2 = (f1 /. 2) `1 by GOBOARD1:def 3;
then A20: (X_axis f1) . 2 = E-bound (L~ f1) by A17, EUCLID:56;
A21: 1 in Seg (len f1) by A4, FINSEQ_1:3;
then A22: 1 in dom f1 by FINSEQ_1:def 3;
then 1 in dom (Y_axis f1) by SPRECT_2:20;
then (Y_axis f1) . 1 = (f1 /. 1) `2 by GOBOARD1:def 4;
then A23: (Y_axis f1) . 1 = N-bound (L~ f1) by A14, EUCLID:56;
(X_axis f1) . 2 = (f1 /. 2) `1 by A19, GOBOARD1:def 3;
then A24: (f1 /. 2) `1 in rng (X_axis f1) by A19, FUNCT_1:def 5;
len (X_axis f1) = len f1 by GOBOARD1:def 3;
then A25: dom (X_axis f1) = Seg (len f1) by FINSEQ_1:def 3;
then (X_axis f1) . 1 = (f1 /. 1) `1 by A21, GOBOARD1:def 3;
then A26: (f1 /. 1) `1 in rng (X_axis f1) by A21, A25, FUNCT_1:def 5;
{((f1 /. 1) `1 ),((f1 /. 2) `1 )} c= rng (X_axis f1)

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in {((f1 /. 1) `1 ),((f1 /. 2) `1 )} or z in rng (X_axis f1) )
assume z in {((f1 /. 1) `1 ),((f1 /. 2) `1 )} ; :: thesis: z in rng (X_axis f1)
hence z in rng (X_axis f1) by A26, A24, TARSKI:def 2; :: thesis: verum

end;

then {((f1 /. 1) `1 )} \/ {((f1 /. 2) `1 )} c= rng (X_axis f1) by ENUMSET1:41;
then A27: card ({((f1 /. 1) `1 )} \/ {((f1 /. 2) `1 )}) <= card (rng (X_axis f1)) by NAT_1:44;
A28: f1 /. (1 + 1) = N-max (L~ f1) by SPRECT_1:92;
then (f1 /. 1) `1 < (f1 /. 2) `1 by A14, SPRECT_2:55;
then not (f1 /. 2) `1 in {((f1 /. 1) `1 )} by TARSKI:def 1;
then A29: card ({((f1 /. 1) `1 )} \/ {((f1 /. 2) `1 )}) = (card {((f1 /. 1) `1 )}) + 1 by CARD_2:54
.= 1 + 1 by CARD_1:50
.= 2 ;
then A30: 1 <> (len (GoB f1)) + 1 by A27, GOBOARD2:24, XREAL_1:31;
2 in dom (Y_axis f1) by A18, SPRECT_2:20;
then (Y_axis f1) . 2 = (f1 /. 2) `2 by GOBOARD1:def 4;
then A31: (Y_axis f1) . 2 = N-bound (L~ f1) by A28, EUCLID:56;
f1 /. 5 = f1 /. 1 by A4, FINSEQ_6:def 1;
then A32: (Y_axis f1) . 5 = N-bound (L~ f1) by A14, A6, EUCLID:56;
A33: rng (Y_axis f1) c= {(S-bound (L~ f1)),(N-bound (L~ f1))}

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng (Y_axis f1) or z in {(S-bound (L~ f1)),(N-bound (L~ f1))} )
assume z in rng (Y_axis f1) ; :: thesis: z in {(S-bound (L~ f1)),(N-bound (L~ f1))}
then consider u being set such that
A34: u in dom (Y_axis f1) and
A35: z = (Y_axis f1) . u by FUNCT_1:def 5;
reconsider mu = u as Element of NAT by A34;
u in dom f1 by A34, SPRECT_2:20;
then u in Seg (len f1) by FINSEQ_1:def 3;
then ( 1 <= mu & mu <= 5 ) by A4, FINSEQ_1:3;
then A36: ( mu = 1 or mu = 1 + 1 or mu = 1 + 2 or mu = 1 + 3 or mu = 1 + 4 ) by Th4;

per cases ( mu = 1 or mu = 2 or mu = 3 or mu = 4 or mu = 5 ) by A36;

suppose mu = 1 ; :: thesis: z in {(S-bound (L~ f1)),(N-bound (L~ f1))}

hence z in {(S-bound (L~ f1)),(N-bound (L~ f1))} by A23, A35, TARSKI:def 2; :: thesis: verum

end;

suppose mu = 2 ; :: thesis: z in {(S-bound (L~ f1)),(N-bound (L~ f1))}

hence z in {(S-bound (L~ f1)),(N-bound (L~ f1))} by A31, A35, TARSKI:def 2; :: thesis: verum

end;

suppose mu = 3 ; :: thesis: z in {(S-bound (L~ f1)),(N-bound (L~ f1))}

hence z in {(S-bound (L~ f1)),(N-bound (L~ f1))} by A10, A35, TARSKI:def 2; :: thesis: verum

end;

suppose mu = 4 ; :: thesis: z in {(S-bound (L~ f1)),(N-bound (L~ f1))}

hence z in {(S-bound (L~ f1)),(N-bound (L~ f1))} by A8, A35, TARSKI:def 2; :: thesis: verum

end;

suppose mu = 5 ; :: thesis: z in {(S-bound (L~ f1)),(N-bound (L~ f1))}

hence z in {(S-bound (L~ f1)),(N-bound (L~ f1))} by A32, A35, TARSKI:def 2; :: thesis: verum

end;

end;

end;

{(S-bound (L~ f1)),(N-bound (L~ f1))} c= rng (Y_axis f1)

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in {(S-bound (L~ f1)),(N-bound (L~ f1))} or z in rng (Y_axis f1) )
assume A37: z in {(S-bound (L~ f1)),(N-bound (L~ f1))} ; :: thesis: z in rng (Y_axis f1)

per cases ( z = S-bound (L~ f1) or z = N-bound (L~ f1) ) by A37, TARSKI:def 2;

suppose A38: z = S-bound (L~ f1) ; :: thesis: z in rng (Y_axis f1)

4 in dom (Y_axis f1) by A7, SPRECT_2:20;
hence z in rng (Y_axis f1) by A8, A38, FUNCT_1:def 5; :: thesis: verum

end;

suppose A39: z = N-bound (L~ f1) ; :: thesis: z in rng (Y_axis f1)

2 in dom (Y_axis f1) by A18, SPRECT_2:20;
hence z in rng (Y_axis f1) by A31, A39, FUNCT_1:def 5; :: thesis: verum

end;

end;

end;

then A40: ( S-bound (L~ f1) < N-bound (L~ f1) & rng (Y_axis f1) = {(S-bound (L~ f1)),(N-bound (L~ f1))} ) by A33, SPRECT_1:34, XBOOLE_0:def 10;
A41: width (GoB f1) = card (rng (Y_axis f1)) by GOBOARD2:24
.= 1 + 1 by A40, CARD_2:76 ;
then A42: width (GoB f1) in Seg (width (GoB f1)) by FINSEQ_1:3;
f1 /. (1 + 1) = E-max (L~ f1) by SPRECT_1:92;
then A43: (SpStSeq D) /. 2 = |[((E-max (L~ (SpStSeq D))) `1 ),((N-max (L~ (SpStSeq D))) `2 )]| by A28, EUCLID:57;
A44: f1 /. 1 = W-max (L~ f1) by SPRECT_1:91;
then (SpStSeq D) /. 1 = |[((W-max (L~ (SpStSeq D))) `1 ),((N-min (L~ (SpStSeq D))) `2 )]| by A14, EUCLID:57;
then ((SpStSeq D) /. 1) + ((SpStSeq D) /. 2) = |[(((W-max (L~ (SpStSeq D))) `1 ) + ((E-max (L~ (SpStSeq D))) `1 )),(((N-min (L~ (SpStSeq D))) `2 ) + ((N-max (L~ (SpStSeq D))) `2 ))]| by A43, EUCLID:60;
then (1 / 2) * (((SpStSeq D) /. 1) + ((SpStSeq D) /. 2)) = |[((1 / 2) * (((W-max (L~ (SpStSeq D))) `1 ) + ((E-max (L~ (SpStSeq D))) `1 ))),(N-bound (L~ (SpStSeq D)))]| by A3, EUCLID:62;
then A45: |[0 ,((|.((1 / 2) * (((SpStSeq D) /. 1) + ((SpStSeq D) /. 2))).| + r) + 1)]| + ((1 / 2) * (((SpStSeq D) /. 1) + ((SpStSeq D) /. 2))) = |[(0 + ((1 / 2) * (((W-max (L~ (SpStSeq D))) `1 ) + ((E-max (L~ (SpStSeq D))) `1 )))),(((|.((1 / 2) * (((SpStSeq D) /. 1) + ((SpStSeq D) /. 2))).| + r) + 1) + (N-bound (L~ (SpStSeq D))))]| by EUCLID:60
.= |[((1 / 2) * (((W-max (L~ (SpStSeq D))) `1 ) + ((E-max (L~ (SpStSeq D))) `1 ))),(((|.((1 / 2) * (((SpStSeq D) /. 1) + ((SpStSeq D) /. 2))).| + r) + 1) + (N-bound (L~ (SpStSeq D))))]| ;
(W-max (L~ (SpStSeq D))) `1 = W-bound (L~ (SpStSeq D)) by EUCLID:56;
then A46: (W-max (L~ (SpStSeq D))) `1 < (E-max (L~ (SpStSeq D))) `1 by A1, EUCLID:56;
A47: f1 /. 1 = W-max (L~ f1) by SPRECT_1:91;
then A48: ((GoB f1) * 1,1) `1 <= (W-max (L~ (SpStSeq D))) `1 by A4, A41, JORDAN5D:7;
then ((GoB f1) * 1,1) `1 < (E-max (L~ (SpStSeq D))) `1 by A46, XXREAL_0:2;
then (((GoB f1) * 1,1) `1 ) + (((GoB f1) * 1,1) `1 ) < ((W-max (L~ (SpStSeq D))) `1 ) + ((E-max (L~ (SpStSeq D))) `1 ) by A48, XREAL_1:10;
then A49: (1 / 2) * (2 * (((GoB f1) * 1,1) `1 )) < (1 / 2) * (((W-max (L~ (SpStSeq D))) `1 ) + ((E-max (L~ (SpStSeq D))) `1 )) by XREAL_1:70;
1 in dom (X_axis f1) by A22, SPRECT_2:19;
then (X_axis f1) . 1 = (f1 /. 1) `1 by GOBOARD1:def 3;
then A50: (X_axis f1) . 1 = W-bound (L~ f1) by A47, EUCLID:56;
f1 /. 5 = W-max (L~ f1) by A4, A44, FINSEQ_6:def 1;
then A51: (X_axis f1) . 5 = W-bound (L~ f1) by A12, EUCLID:56;
A52: rng (X_axis f1) c= {(W-bound (L~ f1)),(E-bound (L~ f1))}

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng (X_axis f1) or z in {(W-bound (L~ f1)),(E-bound (L~ f1))} )
assume z in rng (X_axis f1) ; :: thesis: z in {(W-bound (L~ f1)),(E-bound (L~ f1))}
then consider u being set such that
A53: u in dom (X_axis f1) and
A54: z = (X_axis f1) . u by FUNCT_1:def 5;
reconsider mu = u as Element of NAT by A53;
u in dom f1 by A53, SPRECT_2:19;
then u in Seg (len f1) by FINSEQ_1:def 3;
then ( 1 <= mu & mu <= 5 ) by A4, FINSEQ_1:3;
then A55: ( mu = 1 or mu = 1 + 1 or mu = 1 + 2 or mu = 1 + 3 or mu = 1 + 4 ) by Th4;

per cases ( mu = 1 or mu = 2 or mu = 3 or mu = 4 or mu = 5 ) by A55;

suppose mu = 1 ; :: thesis: z in {(W-bound (L~ f1)),(E-bound (L~ f1))}

hence z in {(W-bound (L~ f1)),(E-bound (L~ f1))} by A50, A54, TARSKI:def 2; :: thesis: verum

end;

suppose mu = 2 ; :: thesis: z in {(W-bound (L~ f1)),(E-bound (L~ f1))}

hence z in {(W-bound (L~ f1)),(E-bound (L~ f1))} by A20, A54, TARSKI:def 2; :: thesis: verum

end;

suppose mu = 3 ; :: thesis: z in {(W-bound (L~ f1)),(E-bound (L~ f1))}

hence z in {(W-bound (L~ f1)),(E-bound (L~ f1))} by A11, A54, TARSKI:def 2; :: thesis: verum

end;

suppose mu = 4 ; :: thesis: z in {(W-bound (L~ f1)),(E-bound (L~ f1))}

hence z in {(W-bound (L~ f1)),(E-bound (L~ f1))} by A15, A54, TARSKI:def 2; :: thesis: verum

end;

suppose mu = 5 ; :: thesis: z in {(W-bound (L~ f1)),(E-bound (L~ f1))}

hence z in {(W-bound (L~ f1)),(E-bound (L~ f1))} by A51, A54, TARSKI:def 2; :: thesis: verum

end;

end;

end;

{(W-bound (L~ f1)),(E-bound (L~ f1))} c= rng (X_axis f1)

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in {(W-bound (L~ f1)),(E-bound (L~ f1))} or z in rng (X_axis f1) )
assume A56: z in {(W-bound (L~ f1)),(E-bound (L~ f1))} ; :: thesis: z in rng (X_axis f1)

per cases ( z = W-bound (L~ f1) or z = E-bound (L~ f1) ) by A56, TARSKI:def 2;

suppose A57: z = W-bound (L~ f1) ; :: thesis: z in rng (X_axis f1)

1 in dom (X_axis f1) by A22, SPRECT_2:19;
hence z in rng (X_axis f1) by A50, A57, FUNCT_1:def 5; :: thesis: verum

end;

suppose A58: z = E-bound (L~ f1) ; :: thesis: z in rng (X_axis f1)

2 in dom (X_axis f1) by A18, SPRECT_2:19;
hence z in rng (X_axis f1) by A20, A58, FUNCT_1:def 5; :: thesis: verum

end;

end;

end;

then A59: rng (X_axis f1) = {(W-bound (L~ f1)),(E-bound (L~ f1))} by A52, XBOOLE_0:def 10;
A60: len (GoB f1) = card (rng (X_axis f1)) by GOBOARD2:24
.= 1 + 1 by A1, A59, CARD_2:76 ;
then A61: ((GoB f1) * (1 + 1),1) `1 >= (E-max (L~ (SpStSeq D))) `1 by A4, A17, A41, JORDAN5D:7;
then (W-max (L~ (SpStSeq D))) `1 < ((GoB f1) * (1 + 1),1) `1 by A46, XXREAL_0:2;
then ((W-max (L~ (SpStSeq D))) `1 ) + ((E-max (L~ (SpStSeq D))) `1 ) < (((GoB f1) * (1 + 1),1) `1 ) + (((GoB f1) * (1 + 1),1) `1 ) by A61, XREAL_1:10;
then A62: (1 / 2) * (((W-max (L~ (SpStSeq D))) `1 ) + ((E-max (L~ (SpStSeq D))) `1 )) < (1 / 2) * (2 * (((GoB f1) * (1 + 1),1) `1 )) by XREAL_1:70;
A63: card (rng (X_axis f1)) = 2 by A1, A59, CARD_2:76;
for p being FinSequence of the carrier of (TOP-REAL 2) st p in rng (GoB f1) holds
len p = 2

proof

len (GoB (Incr (X_axis f1)),(Incr (Y_axis f1))) = len (Incr (X_axis f1)) by GOBOARD2:def 1
.= 2 by A63, SEQ_4:def 25 ;
then consider s1 being FinSequence such that
A64: s1 in rng (GoB (Incr (X_axis f1)),(Incr (Y_axis f1))) and
A65: len s1 = width (GoB (Incr (X_axis f1)),(Incr (Y_axis f1))) by MATRIX_1:def 4;
let p be FinSequence of the carrier of (TOP-REAL 2); :: thesis: ( p in rng (GoB f1) implies len p = 2 )
consider n being Nat such that
A66: for x being set st x in rng (GoB f1) holds
ex s being FinSequence st
( s = x & len s = n ) by MATRIX_1:def 1;
assume p in rng (GoB f1) ; :: thesis: len p = 2
then A67: ex s2 being FinSequence st
( s2 = p & len s2 = n ) by A66;
ex s being FinSequence st
( s = s1 & len s = n ) by A16, A64, A66;
hence len p = 2 by A41, A65, A67, GOBOARD2:def 3; :: thesis: verum

end;

then A68: GoB f1 is Matrix of 2,2,the carrier of (TOP-REAL 2) by A60, MATRIX_1:def 3;
len (GoB f1) in Seg (len (GoB f1)) by A60, FINSEQ_1:3;
then [(len (GoB f1)),(width (GoB f1))] in [:(Seg (len (GoB f1))),(Seg (width (GoB f1))):] by A42, ZFMISC_1:106;
then A69: [(len (GoB f1)),(width (GoB f1))] in Indices (GoB f1) by A60, A41, A68, MATRIX_1:25;
1 in Seg (len (GoB f1)) by A60, FINSEQ_1:3;
then [1,(width (GoB f1))] in [:(Seg (len (GoB f1))),(Seg (width (GoB f1))):] by A42, ZFMISC_1:106;
then A70: [1,(width (GoB f1))] in Indices (GoB f1) by A60, A41, A68, MATRIX_1:25;
card (rng (X_axis f1)) > 1 by A27, A29, XXREAL_0:2;
then A71: 1 < len (GoB f1) by GOBOARD2:24;
A72: f1 /. 1 = (GoB f1) * 1,(width (GoB f1)) by A41, Th97;
set p = |[0 ,((|.((1 / 2) * (((SpStSeq D) /. 1) + ((SpStSeq D) /. 2))).| + r) + 1)]|;
A73: ( |[0 ,((|.((1 / 2) * (((SpStSeq D) /. 1) + ((SpStSeq D) /. 2))).| + r) + 1)]| `1 = 0 & |[0 ,((|.((1 / 2) * (((SpStSeq D) /. 1) + ((SpStSeq D) /. 2))).| + r) + 1)]| `2 = (|.((1 / 2) * (((SpStSeq D) /. 1) + ((SpStSeq D) /. 2))).| + r) + 1 ) by EUCLID:56;
A74: ( |.(|[0 ,((|.((1 / 2) * (((SpStSeq D) /. 1) + ((SpStSeq D) /. 2))).| + r) + 1)]| + ((1 / 2) * (((SpStSeq D) /. 1) + ((SpStSeq D) /. 2)))).| >= |.|[0 ,((|.((1 / 2) * (((SpStSeq D) /. 1) + ((SpStSeq D) /. 2))).| + r) + 1)]|.| - |.((1 / 2) * (((SpStSeq D) /. 1) + ((SpStSeq D) /. 2))).| & r < r + 1 ) by TOPRNS_1:32, XREAL_1:31;
A75: Int (left_cell f1,1) c= LeftComp (SpStSeq D) by GOBOARD9:def 1;
A76: width (GoB f1) <> (width (GoB f1)) + 1 ;
f1 /. (1 + 1) = (GoB f1) * (len (GoB f1)),(width (GoB f1)) by A60, A41, Th97;
then left_cell f1,1 = cell (GoB f1),1,(width (GoB f1)) by A4, A70, A69, A72, A30, A76, GOBOARD5:def 7;
then A77: Int (left_cell f1,1) = { |[r2,s]| where r2, s is Real : ( ((GoB f1) * 1,1) `1 < r2 & r2 < ((GoB f1) * (1 + 1),1) `1 & ((GoB f1) * 1,(width (GoB f1))) `2 < s ) } by A71, GOBOARD6:28;
A78: |.q4.| < r by A13;
A79: |.|[0 ,((|.((1 / 2) * (((SpStSeq D) /. 1) + ((SpStSeq D) /. 2))).| + r) + 1)]|.| = sqrt (((|[0 ,((|.((1 / 2) * (((SpStSeq D) /. 1) + ((SpStSeq D) /. 2))).| + r) + 1)]| `1 ) ^2 ) + ((|[0 ,((|.((1 / 2) * (((SpStSeq D) /. 1) + ((SpStSeq D) /. 2))).| + r) + 1)]| `2 ) ^2 )) by JGRAPH_1:47
.= (|.((1 / 2) * (((SpStSeq D) /. 1) + ((SpStSeq D) /. 2))).| + r) + 1 by A78, A73, SQUARE_1:89 ;
((GoB f1) * 1,(width (GoB f1))) `2 < (N-bound (L~ (SpStSeq D))) + ((|.((1 / 2) * (((SpStSeq D) /. 1) + ((SpStSeq D) /. 2))).| + r) + 1) by A78, A14, A72, A2, XREAL_1:31;
then |[0 ,((|.((1 / 2) * (((SpStSeq D) /. 1) + ((SpStSeq D) /. 2))).| + r) + 1)]| + ((1 / 2) * (((SpStSeq D) /. 1) + ((SpStSeq D) /. 2))) in Int (left_cell f1,1) by A77, A45, A49, A62;
hence contradiction by A13, A79, A74, A75, XXREAL_0:2; :: thesis: verum