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;
set q3 = the Element of LeftComp (SpStSeq D);
reconsider q4 = the Element of LeftComp (SpStSeq D) as Point of (TOP-REAL 2) ;
set r1 = |.((1 / 2) * (((SpStSeq D) /. 1) + ((SpStSeq D) /. 2))).|;
reconsider f1 = SpStSeq D as constant standard special_circular_sequence ;
A1: W-bound (L~ f1) < E-bound (L~ f1) by SPRECT_1:31;
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:82;
then 5 in Seg (len f1) by FINSEQ_1:1;
then A5: 5 in dom f1 by FINSEQ_1:def 3;
then 5 in dom (Y_axis f1) by SPRECT_2:16;
then A6: (Y_axis f1) . 5 = (f1 /. 5) `2 by GOBOARD1:def 2;
4 in Seg (len f1) by A4, FINSEQ_1:1;
then A7: 4 in dom f1 by FINSEQ_1:def 3;
then 4 in dom (Y_axis f1) by SPRECT_2:16;
then ( f1 /. 4 = S-min (L~ f1) & (Y_axis f1) . 4 = (f1 /. 4) `2 ) by GOBOARD1:def 2, SPRECT_1:86;
then A8: (Y_axis f1) . 4 = S-bound (L~ f1) ;
3 in Seg (len f1) by A4, FINSEQ_1:1;
then A9: 3 in dom f1 by FINSEQ_1:def 3;
then 3 in dom (Y_axis f1) by SPRECT_2:16;
then ( f1 /. 3 = S-max (L~ f1) & (Y_axis f1) . 3 = (f1 /. 3) `2 ) by GOBOARD1:def 2, SPRECT_1:85;
then A10: (Y_axis f1) . 3 = S-bound (L~ f1) ;
3 in dom (X_axis f1) by A9, SPRECT_2:15;
then ( f1 /. 3 = E-min (L~ f1) & (X_axis f1) . 3 = (f1 /. 3) `1 ) by GOBOARD1:def 1, SPRECT_1:85;
then A11: (X_axis f1) . 3 = E-bound (L~ f1) ;
5 in dom (X_axis f1) by A5, SPRECT_2:15;
then A12: (X_axis f1) . 5 = (f1 /. 5) `1 by GOBOARD1:def 1;
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 Th21;
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:83;
4 in dom (X_axis f1) by A7, SPRECT_2:15;
then ( f1 /. 4 = W-min (L~ f1) & (X_axis f1) . 4 = (f1 /. 4) `1 ) by GOBOARD1:def 1, SPRECT_1:86;
then A15: (X_axis f1) . 4 = W-bound (L~ f1) ;
A16: GoB f1 = GoB ((Incr (X_axis f1)),(Incr (Y_axis f1))) by GOBOARD2:def 2;
A17: f1 /. 2 = E-max (L~ f1) by SPRECT_1:84;
2 in Seg (len f1) by A4, FINSEQ_1:1;
then A18: 2 in dom f1 by FINSEQ_1:def 3;
then A19: 2 in dom (X_axis f1) by SPRECT_2:15;
then (X_axis f1) . 2 = (f1 /. 2) `1 by GOBOARD1:def 1;
then A20: (X_axis f1) . 2 = E-bound (L~ f1) by A17;
A21: 1 in Seg (len f1) by A4, FINSEQ_1:1;
then A22: 1 in dom f1 by FINSEQ_1:def 3;
then 1 in dom (Y_axis f1) by SPRECT_2:16;
then (Y_axis f1) . 1 = (f1 /. 1) `2 by GOBOARD1:def 2;
then A23: (Y_axis f1) . 1 = N-bound (L~ f1) by A14;
(X_axis f1) . 2 = (f1 /. 2) `1 by A19, GOBOARD1:def 1;
then A24: (f1 /. 2) `1 in rng (X_axis f1) by A19, FUNCT_1:def 3;
len (X_axis f1) = len f1 by GOBOARD1:def 1;
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 1;
then A26: (f1 /. 1) `1 in rng (X_axis f1) by A21, A25, FUNCT_1:def 3;
{((f1 /. 1) `1),((f1 /. 2) `1)} c= rng (X_axis f1) by A26, A24, TARSKI:def 2;
then {((f1 /. 1) `1)} \/ {((f1 /. 2) `1)} c= rng (X_axis f1) by ENUMSET1:1;
then A27: card ({((f1 /. 1) `1)} \/ {((f1 /. 2) `1)}) <= card (rng (X_axis f1)) by NAT_1:43;
A28: f1 /. (1 + 1) = N-max (L~ f1) by SPRECT_1:84;
then (f1 /. 1) `1 < (f1 /. 2) `1 by A14, SPRECT_2:51;
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:41
.= 1 + 1 by CARD_1:30
.= 2 ;
A30: 1 <> (len (GoB f1)) + 1 by A27, GOBOARD2:13, XREAL_1:29;
2 in dom (Y_axis f1) by A18, SPRECT_2:16;
then (Y_axis f1) . 2 = (f1 /. 2) `2 by GOBOARD1:def 2;
then A31: (Y_axis f1) . 2 = N-bound (L~ f1) by A28;
f1 /. 5 = f1 /. 1 by A4, FINSEQ_6:def 1;
then A32: (Y_axis f1) . 5 = N-bound (L~ f1) by A14, A6;
A33: rng (Y_axis f1) c= {(S-bound (L~ f1)),(N-bound (L~ f1))}

proof

let z be object ; :: 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 object such that
A34: u in dom (Y_axis f1) and
A35: z = (Y_axis f1) . u by FUNCT_1:def 3;
reconsider mu = u as Element of NAT by A34;
u in dom f1 by A34, SPRECT_2:16;
then u in Seg (len f1) by FINSEQ_1:def 3;
then ( 1 <= mu & mu <= 5 ) by A4, FINSEQ_1:1;
then A36: not not mu = 1 + 0 & ... & not mu = 1 + 4 by NAT_1:62;

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 object ; :: 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:16;
hence z in rng (Y_axis f1) by A8, A38, FUNCT_1:def 3; :: 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:16;
hence z in rng (Y_axis f1) by A31, A39, FUNCT_1:def 3; :: 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:32;
A41: width (GoB f1) = card (rng (Y_axis f1)) by GOBOARD2:13
.= 1 + 1 by A40, CARD_2:57 ;
then A42: width (GoB f1) in Seg (width (GoB f1)) by FINSEQ_1:1;
f1 /. (1 + 1) = E-max (L~ f1) by SPRECT_1:84;
then A43: (SpStSeq D) /. 2 = |[((E-max (L~ (SpStSeq D))) `1),((N-max (L~ (SpStSeq D))) `2)]| by A28;
A44: f1 /. 1 = W-max (L~ f1) by SPRECT_1:83;
then (SpStSeq D) /. 1 = |[((W-max (L~ (SpStSeq D))) `1),((N-min (L~ (SpStSeq D))) `2)]| by A14;
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:56;
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:58;
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:56
.= |[((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))))]| ;
A46: (W-max (L~ (SpStSeq D))) `1 < (E-max (L~ (SpStSeq D))) `1 by A1;
A47: f1 /. 1 = W-max (L~ f1) by SPRECT_1:83;
then A48: ((GoB f1) * (1,1)) `1 <= (W-max (L~ (SpStSeq D))) `1 by A4, A41, JORDAN5D:5;
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:8;
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:68;
1 in dom (X_axis f1) by A22, SPRECT_2:15;
then (X_axis f1) . 1 = (f1 /. 1) `1 by GOBOARD1:def 1;
then A50: (X_axis f1) . 1 = W-bound (L~ f1) by A47;
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;
A52: rng (X_axis f1) c= {(W-bound (L~ f1)),(E-bound (L~ f1))}

proof

let z be object ; :: 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 object such that
A53: u in dom (X_axis f1) and
A54: z = (X_axis f1) . u by FUNCT_1:def 3;
reconsider mu = u as Element of NAT by A53;
u in dom f1 by A53, SPRECT_2:15;
then u in Seg (len f1) by FINSEQ_1:def 3;
then ( 1 <= mu & mu <= 5 ) by A4, FINSEQ_1:1;
then A55: not not mu = 1 + 0 & ... & not mu = 1 + 4 by NAT_1:62;

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 object ; :: 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:15;
hence z in rng (X_axis f1) by A50, A57, FUNCT_1:def 3; :: 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:15;
hence z in rng (X_axis f1) by A20, A58, FUNCT_1:def 3; :: thesis: verum

end;

end;

end;

then A59: rng (X_axis f1) = {(W-bound (L~ f1)),(E-bound (L~ f1))} by A52;
A60: len (GoB f1) = card (rng (X_axis f1)) by GOBOARD2:13
.= 1 + 1 by A1, A59, CARD_2:57 ;
then A61: ((GoB f1) * ((1 + 1),1)) `1 >= (E-max (L~ (SpStSeq D))) `1 by A4, A17, A41, JORDAN5D:5;
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:8;
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:68;
A63: card (rng (X_axis f1)) = 2 by A1, A59, CARD_2:57;
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 21 ;
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_0:def 3;
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 object st x in rng (GoB f1) holds
ex s being FinSequence st
( s = x & len s = n ) by MATRIX_0: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 2; :: thesis: verum

end;

then A68: GoB f1 is Matrix of 2,2, the carrier of (TOP-REAL 2) by A60, MATRIX_0:def 2;
len (GoB f1) in Seg (len (GoB f1)) by A60, FINSEQ_1:1;
then [(len (GoB f1)),(width (GoB f1))] in [:(Seg (len (GoB f1))),(Seg (width (GoB f1))):] by A42, ZFMISC_1:87;
then A69: [(len (GoB f1)),(width (GoB f1))] in Indices (GoB f1) by A60, A41, A68, MATRIX_0:24;
1 in Seg (len (GoB f1)) by A60, FINSEQ_1:1;
then [1,(width (GoB f1))] in [:(Seg (len (GoB f1))),(Seg (width (GoB f1))):] by A42, ZFMISC_1:87;
then A70: [1,(width (GoB f1))] in Indices (GoB f1) by A60, A41, A68, MATRIX_0:24;
card (rng (X_axis f1)) > 1 by A27, A29, XXREAL_0:2;
then A71: 1 < len (GoB f1) by GOBOARD2:13;
A72: f1 /. 1 = (GoB f1) * (1,(width (GoB f1))) by A41, Th73;
set p = |[0,((|.((1 / 2) * (((SpStSeq D) /. 1) + ((SpStSeq D) /. 2))).| + r) + 1)]|;
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:31, XREAL_1:29;
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, Th73;
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:25;
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:30
.= (|.((1 / 2) * (((SpStSeq D) /. 1) + ((SpStSeq D) /. 2))).| + r) + 1 by A78, SQUARE_1:22 ;
((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, XREAL_1:29;
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