let D be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ( len (GoB (SpStSeq D)) = 2 & width (GoB (SpStSeq D)) = 2 & (SpStSeq D) /. 1 = (GoB (SpStSeq D)) * 1,2 & (SpStSeq D) /. 2 = (GoB (SpStSeq D)) * 2,2 & (SpStSeq D) /. 3 = (GoB (SpStSeq D)) * 2,1 & (SpStSeq D) /. 4 = (GoB (SpStSeq D)) * 1,1 & (SpStSeq D) /. 5 = (GoB (SpStSeq D)) * 1,2 )
set f = SpStSeq D;
A1: S-bound (L~ (SpStSeq D)) < N-bound (L~ (SpStSeq D)) by SPRECT_1:34;
A2: len (SpStSeq D) = 5 by SPRECT_1:90;
then A3: (SpStSeq D) /. 5 = (SpStSeq D) /. 1 by FINSEQ_6:def 1;
4 in Seg (len (SpStSeq D)) by A2, FINSEQ_1:3;
then A4: 4 in dom (SpStSeq D) by FINSEQ_1:def 3;
then 4 in dom (X_axis (SpStSeq D)) by SPRECT_2:19;
then ( (SpStSeq D) /. 4 = W-min (L~ (SpStSeq D)) & (X_axis (SpStSeq D)) . 4 = ((SpStSeq D) /. 4) `1 ) by GOBOARD1:def 3, SPRECT_1:94;
then A5: (X_axis (SpStSeq D)) . 4 = W-bound (L~ (SpStSeq D)) by EUCLID:56;
A6: (SpStSeq D) /. 3 = S-max (L~ (SpStSeq D)) by SPRECT_1:93;
3 in Seg (len (SpStSeq D)) by A2, FINSEQ_1:3;
then A7: 3 in dom (SpStSeq D) by FINSEQ_1:def 3;
then 3 in dom (X_axis (SpStSeq D)) by SPRECT_2:19;
then ( (SpStSeq D) /. 3 = E-min (L~ (SpStSeq D)) & (X_axis (SpStSeq D)) . 3 = ((SpStSeq D) /. 3) `1 ) by GOBOARD1:def 3, SPRECT_1:93;
then A8: (X_axis (SpStSeq D)) . 3 = E-bound (L~ (SpStSeq D)) by EUCLID:56;
A9: (SpStSeq D) /. (1 + 1) = N-max (L~ (SpStSeq D)) by SPRECT_1:92;
3 in dom (Y_axis (SpStSeq D)) by A7, SPRECT_2:20;
then (Y_axis (SpStSeq D)) . 3 = ((SpStSeq D) /. 3) `2 by GOBOARD1:def 4;
then A10: (Y_axis (SpStSeq D)) . 3 = S-bound (L~ (SpStSeq D)) by A6, EUCLID:56;
A11: (SpStSeq D) /. 1 = N-min (L~ (SpStSeq D)) by SPRECT_1:91;
1 in Seg (len (SpStSeq D)) by A2, FINSEQ_1:3;
then A12: 1 in dom (SpStSeq D) by FINSEQ_1:def 3;
then 1 in dom (Y_axis (SpStSeq D)) by SPRECT_2:20;
then (Y_axis (SpStSeq D)) . 1 = ((SpStSeq D) /. 1) `2 by GOBOARD1:def 4;
then A13: (Y_axis (SpStSeq D)) . 1 = N-bound (L~ (SpStSeq D)) by A11, EUCLID:56;
A14: (SpStSeq D) /. 4 = S-min (L~ (SpStSeq D)) by SPRECT_1:94;
2 in Seg (len (SpStSeq D)) by A2, FINSEQ_1:3;
then A15: 2 in dom (SpStSeq D) by FINSEQ_1:def 3;
then 2 in dom (X_axis (SpStSeq D)) by SPRECT_2:19;
then ( (SpStSeq D) /. (1 + 1) = E-max (L~ (SpStSeq D)) & (X_axis (SpStSeq D)) . 2 = ((SpStSeq D) /. 2) `1 ) by GOBOARD1:def 3, SPRECT_1:92;
then A16: (X_axis (SpStSeq D)) . 2 = E-bound (L~ (SpStSeq D)) by EUCLID:56;
4 in dom (Y_axis (SpStSeq D)) by A4, SPRECT_2:20;
then (Y_axis (SpStSeq D)) . 4 = ((SpStSeq D) /. 4) `2 by GOBOARD1:def 4;
then A17: (Y_axis (SpStSeq D)) . 4 = S-bound (L~ (SpStSeq D)) by A14, EUCLID:56;
2 in dom (Y_axis (SpStSeq D)) by A15, SPRECT_2:20;
then (Y_axis (SpStSeq D)) . 2 = ((SpStSeq D) /. 2) `2 by GOBOARD1:def 4;
then A18: (Y_axis (SpStSeq D)) . 2 = N-bound (L~ (SpStSeq D)) by A9, EUCLID:56;
A19: {(S-bound (L~ (SpStSeq D))),(N-bound (L~ (SpStSeq D)))} c= rng (Y_axis (SpStSeq D))

proof

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

now

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

case A21: z = S-bound (L~ (SpStSeq D)) ; :: thesis: z in rng (Y_axis (SpStSeq D))

4 in dom (Y_axis (SpStSeq D)) by A4, SPRECT_2:20;
hence z in rng (Y_axis (SpStSeq D)) by A17, A21, FUNCT_1:def 5; :: thesis: verum

end;

case A22: z = N-bound (L~ (SpStSeq D)) ; :: thesis: z in rng (Y_axis (SpStSeq D))

2 in dom (Y_axis (SpStSeq D)) by A15, SPRECT_2:20;
hence z in rng (Y_axis (SpStSeq D)) by A18, A22, FUNCT_1:def 5; :: thesis: verum

end;

end;

end;

hence z in rng (Y_axis (SpStSeq D)) ; :: thesis: verum

end;

A23: (SpStSeq D) /. 1 = W-max (L~ (SpStSeq D)) by SPRECT_1:91;
1 in dom (X_axis (SpStSeq D)) by A12, SPRECT_2:19;
then (X_axis (SpStSeq D)) . 1 = ((SpStSeq D) /. 1) `1 by GOBOARD1:def 3;
then A24: (X_axis (SpStSeq D)) . 1 = W-bound (L~ (SpStSeq D)) by A23, EUCLID:56;
A25: {(W-bound (L~ (SpStSeq D))),(E-bound (L~ (SpStSeq D)))} c= rng (X_axis (SpStSeq D))

proof

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

now

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

case A27: z = W-bound (L~ (SpStSeq D)) ; :: thesis: z in rng (X_axis (SpStSeq D))

1 in dom (X_axis (SpStSeq D)) by A12, SPRECT_2:19;
hence z in rng (X_axis (SpStSeq D)) by A24, A27, FUNCT_1:def 5; :: thesis: verum

end;

case A28: z = E-bound (L~ (SpStSeq D)) ; :: thesis: z in rng (X_axis (SpStSeq D))

2 in dom (X_axis (SpStSeq D)) by A15, SPRECT_2:19;
hence z in rng (X_axis (SpStSeq D)) by A16, A28, FUNCT_1:def 5; :: thesis: verum

end;

end;

end;

hence z in rng (X_axis (SpStSeq D)) ; :: thesis: verum

end;

A29: GoB (SpStSeq D) = GoB (Incr (X_axis (SpStSeq D))),(Incr (Y_axis (SpStSeq D))) by GOBOARD2:def 3;
5 in Seg (len (SpStSeq D)) by A2, FINSEQ_1:3;
then A30: 5 in dom (SpStSeq D) by FINSEQ_1:def 3;
then 5 in dom (X_axis (SpStSeq D)) by SPRECT_2:19;
then (X_axis (SpStSeq D)) . 5 = ((SpStSeq D) /. 5) `1 by GOBOARD1:def 3;
then A31: (X_axis (SpStSeq D)) . 5 = W-bound (L~ (SpStSeq D)) by A23, A3, EUCLID:56;
rng (X_axis (SpStSeq D)) c= {(W-bound (L~ (SpStSeq D))),(E-bound (L~ (SpStSeq D)))}

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng (X_axis (SpStSeq D)) or z in {(W-bound (L~ (SpStSeq D))),(E-bound (L~ (SpStSeq D)))} )
assume z in rng (X_axis (SpStSeq D)) ; :: thesis: z in {(W-bound (L~ (SpStSeq D))),(E-bound (L~ (SpStSeq D)))}
then consider u being set such that
A32: u in dom (X_axis (SpStSeq D)) and
A33: z = (X_axis (SpStSeq D)) . u by FUNCT_1:def 5;
reconsider mu = u as Element of NAT by A32;
u in dom (SpStSeq D) by A32, SPRECT_2:19;
then u in Seg (len (SpStSeq D)) by FINSEQ_1:def 3;
then ( 1 <= mu & mu <= 5 ) by A2, FINSEQ_1:3;
then A34: ( 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 A34;

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

hence z in {(W-bound (L~ (SpStSeq D))),(E-bound (L~ (SpStSeq D)))} by A24, A33, TARSKI:def 2; :: thesis: verum

end;

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

hence z in {(W-bound (L~ (SpStSeq D))),(E-bound (L~ (SpStSeq D)))} by A16, A33, TARSKI:def 2; :: thesis: verum

end;

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

hence z in {(W-bound (L~ (SpStSeq D))),(E-bound (L~ (SpStSeq D)))} by A8, A33, TARSKI:def 2; :: thesis: verum

end;

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

hence z in {(W-bound (L~ (SpStSeq D))),(E-bound (L~ (SpStSeq D)))} by A5, A33, TARSKI:def 2; :: thesis: verum

end;

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

hence z in {(W-bound (L~ (SpStSeq D))),(E-bound (L~ (SpStSeq D)))} by A31, A33, TARSKI:def 2; :: thesis: verum

end;

end;

end;

then A35: rng (X_axis (SpStSeq D)) = {(W-bound (L~ (SpStSeq D))),(E-bound (L~ (SpStSeq D)))} by A25, XBOOLE_0:def 10;
then A36: rng (Incr (X_axis (SpStSeq D))) = {(W-bound (L~ (SpStSeq D))),(E-bound (L~ (SpStSeq D)))} by SEQ_4:def 25;
5 in dom (Y_axis (SpStSeq D)) by A30, SPRECT_2:20;
then (Y_axis (SpStSeq D)) . 5 = ((SpStSeq D) /. 5) `2 by GOBOARD1:def 4;
then A37: (Y_axis (SpStSeq D)) . 5 = N-bound (L~ (SpStSeq D)) by A11, A3, EUCLID:56;
rng (Y_axis (SpStSeq D)) c= {(S-bound (L~ (SpStSeq D))),(N-bound (L~ (SpStSeq D)))}

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in rng (Y_axis (SpStSeq D)) or z in {(S-bound (L~ (SpStSeq D))),(N-bound (L~ (SpStSeq D)))} )
assume z in rng (Y_axis (SpStSeq D)) ; :: thesis: z in {(S-bound (L~ (SpStSeq D))),(N-bound (L~ (SpStSeq D)))}
then consider u being set such that
A38: u in dom (Y_axis (SpStSeq D)) and
A39: z = (Y_axis (SpStSeq D)) . u by FUNCT_1:def 5;
reconsider mu = u as Element of NAT by A38;
u in dom (SpStSeq D) by A38, SPRECT_2:20;
then u in Seg (len (SpStSeq D)) by FINSEQ_1:def 3;
then ( 1 <= mu & mu <= 5 ) by A2, FINSEQ_1:3;
then A40: ( 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 A40;

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

hence z in {(S-bound (L~ (SpStSeq D))),(N-bound (L~ (SpStSeq D)))} by A13, A39, TARSKI:def 2; :: thesis: verum

end;

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

hence z in {(S-bound (L~ (SpStSeq D))),(N-bound (L~ (SpStSeq D)))} by A18, A39, TARSKI:def 2; :: thesis: verum

end;

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

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

end;

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

hence z in {(S-bound (L~ (SpStSeq D))),(N-bound (L~ (SpStSeq D)))} by A17, A39, TARSKI:def 2; :: thesis: verum

end;

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

hence z in {(S-bound (L~ (SpStSeq D))),(N-bound (L~ (SpStSeq D)))} by A37, A39, TARSKI:def 2; :: thesis: verum

end;

end;

end;

then A41: rng (Y_axis (SpStSeq D)) = {(S-bound (L~ (SpStSeq D))),(N-bound (L~ (SpStSeq D)))} by A19, XBOOLE_0:def 10;
then card (rng (Y_axis (SpStSeq D))) = 2 by A1, CARD_2:76;
then A42: len (Incr (Y_axis (SpStSeq D))) = 2 by SEQ_4:def 25;
A43: W-bound (L~ (SpStSeq D)) < E-bound (L~ (SpStSeq D)) by SPRECT_1:33;
then A44: card (rng (X_axis (SpStSeq D))) = 2 by A35, CARD_2:76;
then A45: len (Incr (X_axis (SpStSeq D))) = 2 by SEQ_4:def 25;
A46: len (GoB (SpStSeq D)) = card (rng (X_axis (SpStSeq D))) by GOBOARD2:24
.= 1 + 1 by A43, A35, CARD_2:76 ;
then A47: 1 in Seg (len (GoB (SpStSeq D))) by FINSEQ_1:3;
A48: width (GoB (SpStSeq D)) = card (rng (Y_axis (SpStSeq D))) by GOBOARD2:24
.= 1 + 1 by A1, A41, CARD_2:76 ;
for p being FinSequence of the carrier of (TOP-REAL 2) st p in rng (GoB (SpStSeq D)) holds
len p = 2

proof

len (GoB (Incr (X_axis (SpStSeq D))),(Incr (Y_axis (SpStSeq D)))) = len (Incr (X_axis (SpStSeq D))) by GOBOARD2:def 1
.= 2 by A44, SEQ_4:def 25 ;
then consider s1 being FinSequence such that
A49: s1 in rng (GoB (Incr (X_axis (SpStSeq D))),(Incr (Y_axis (SpStSeq D)))) and
A50: len s1 = width (GoB (Incr (X_axis (SpStSeq D))),(Incr (Y_axis (SpStSeq D)))) by MATRIX_1:def 4;
let p be FinSequence of the carrier of (TOP-REAL 2); :: thesis: ( p in rng (GoB (SpStSeq D)) implies len p = 2 )
consider n being Nat such that
A51: for x being set st x in rng (GoB (SpStSeq D)) holds
ex s being FinSequence st
( s = x & len s = n ) by MATRIX_1:def 1;
assume p in rng (GoB (SpStSeq D)) ; :: thesis: len p = 2
then A52: ex s2 being FinSequence st
( s2 = p & len s2 = n ) by A51;
s1 in rng (GoB (SpStSeq D)) by A49, GOBOARD2:def 3;
then ex s being FinSequence st
( s = s1 & len s = n ) by A51;
hence len p = 2 by A48, A50, A52, GOBOARD2:def 3; :: thesis: verum

end;

then A53: GoB (SpStSeq D) is Matrix of 2,2,the carrier of (TOP-REAL 2) by A46, MATRIX_1:def 3;
A54: 1 in Seg (width (GoB (SpStSeq D))) by A48, FINSEQ_1:3;
then [1,1] in [:(Seg (len (GoB (SpStSeq D)))),(Seg (width (GoB (SpStSeq D)))):] by A47, ZFMISC_1:106;
then A55: [1,1] in Indices (GoB (SpStSeq D)) by A46, A48, A53, MATRIX_1:25;
A56: width (GoB (SpStSeq D)) in Seg (width (GoB (SpStSeq D))) by A48, FINSEQ_1:3;
then [1,(width (GoB (SpStSeq D)))] in [:(Seg (len (GoB (SpStSeq D)))),(Seg (width (GoB (SpStSeq D)))):] by A47, ZFMISC_1:106;
then A57: [1,(width (GoB (SpStSeq D)))] in Indices (GoB (SpStSeq D)) by A46, A48, A53, MATRIX_1:25;
A58: len (GoB (SpStSeq D)) in Seg (len (GoB (SpStSeq D))) by A46, FINSEQ_1:3;
then [(len (GoB (SpStSeq D))),1] in [:(Seg (len (GoB (SpStSeq D)))),(Seg (width (GoB (SpStSeq D)))):] by A54, ZFMISC_1:106;
then A59: [(len (GoB (SpStSeq D))),1] in Indices (GoB (SpStSeq D)) by A46, A48, A53, MATRIX_1:25;
(S-max (L~ (SpStSeq D))) `1 = (SE-corner D) `1 by SPRECT_1:89
.= E-bound D by EUCLID:56
.= E-bound (L~ (SpStSeq D)) by SPRECT_1:69
.= (Incr (X_axis (SpStSeq D))) . 2 by A43, A36, A45, Th8 ;
then (S-max (L~ (SpStSeq D))) `1 = |[((Incr (X_axis (SpStSeq D))) . 2),((Incr (Y_axis (SpStSeq D))) . 1)]| `1 by EUCLID:56;
then A60: (S-max (L~ (SpStSeq D))) `1 = ((GoB (SpStSeq D)) * (len (GoB (SpStSeq D))),1) `1 by A29, A46, A59, GOBOARD2:def 1;
(S-min (L~ (SpStSeq D))) `1 = (SW-corner D) `1 by SPRECT_1:88
.= W-bound D by EUCLID:56
.= W-bound (L~ (SpStSeq D)) by SPRECT_1:66
.= (Incr (X_axis (SpStSeq D))) . 1 by A43, A36, A45, Th8 ;
then (S-min (L~ (SpStSeq D))) `1 = |[((Incr (X_axis (SpStSeq D))) . 1),((Incr (Y_axis (SpStSeq D))) . 1)]| `1 by EUCLID:56;
then A61: (S-min (L~ (SpStSeq D))) `1 = ((GoB (SpStSeq D)) * 1,1) `1 by A29, A55, GOBOARD2:def 1;
[(len (GoB (SpStSeq D))),(width (GoB (SpStSeq D)))] in [:(Seg (len (GoB (SpStSeq D)))),(Seg (width (GoB (SpStSeq D)))):] by A58, A56, ZFMISC_1:106;
then A62: [(len (GoB (SpStSeq D))),(width (GoB (SpStSeq D)))] in Indices (GoB (SpStSeq D)) by A46, A48, A53, MATRIX_1:25;
W-bound (L~ (SpStSeq D)) = (Incr (X_axis (SpStSeq D))) . 1 by A43, A36, A45, Th8;
then (W-max (L~ (SpStSeq D))) `1 = (Incr (X_axis (SpStSeq D))) . 1 by EUCLID:56;
then (W-max (L~ (SpStSeq D))) `1 = |[((Incr (X_axis (SpStSeq D))) . 1),((Incr (Y_axis (SpStSeq D))) . (1 + 1))]| `1 by EUCLID:56;
then A63: (W-max (L~ (SpStSeq D))) `1 = ((GoB (SpStSeq D)) * 1,(width (GoB (SpStSeq D)))) `1 by A29, A48, A57, GOBOARD2:def 1;
A64: ( (SpStSeq D) /. 3 = |[(((SpStSeq D) /. 3) `1 ),(((SpStSeq D) /. 3) `2 )]| & (SpStSeq D) /. 4 = |[(((SpStSeq D) /. 4) `1 ),(((SpStSeq D) /. 4) `2 )]| ) by EUCLID:57;
A65: ( (SpStSeq D) /. 1 = |[(((SpStSeq D) /. 1) `1 ),(((SpStSeq D) /. 1) `2 )]| & (SpStSeq D) /. (1 + 1) = |[(((SpStSeq D) /. (1 + 1)) `1 ),(((SpStSeq D) /. (1 + 1)) `2 )]| ) by EUCLID:57;
A66: rng (Incr (Y_axis (SpStSeq D))) = {(S-bound (L~ (SpStSeq D))),(N-bound (L~ (SpStSeq D)))} by A41, SEQ_4:def 25;
then A67: N-bound (L~ (SpStSeq D)) = (Incr (Y_axis (SpStSeq D))) . 2 by A1, A42, Th8;
then (N-min (L~ (SpStSeq D))) `2 = (Incr (Y_axis (SpStSeq D))) . 2 by EUCLID:56;
then (N-min (L~ (SpStSeq D))) `2 = |[((Incr (X_axis (SpStSeq D))) . 1),((Incr (Y_axis (SpStSeq D))) . 2)]| `2 by EUCLID:56;
then A68: (N-min (L~ (SpStSeq D))) `2 = ((GoB (SpStSeq D)) * 1,(width (GoB (SpStSeq D)))) `2 by A29, A48, A57, GOBOARD2:def 1;
A69: S-bound (L~ (SpStSeq D)) = (Incr (Y_axis (SpStSeq D))) . 1 by A1, A66, A42, Th8;
then (S-min (L~ (SpStSeq D))) `2 = (Incr (Y_axis (SpStSeq D))) . 1 by EUCLID:56;
then (S-min (L~ (SpStSeq D))) `2 = |[((Incr (X_axis (SpStSeq D))) . 1),((Incr (Y_axis (SpStSeq D))) . 1)]| `2 by EUCLID:56;
then A70: (S-min (L~ (SpStSeq D))) `2 = ((GoB (SpStSeq D)) * 1,1) `2 by A29, A55, GOBOARD2:def 1;
(N-max (L~ (SpStSeq D))) `2 = N-bound (L~ (SpStSeq D)) by EUCLID:56;
then (N-max (L~ (SpStSeq D))) `2 = |[((Incr (X_axis (SpStSeq D))) . 2),((Incr (Y_axis (SpStSeq D))) . 2)]| `2 by A67, EUCLID:56;
then A71: (N-max (L~ (SpStSeq D))) `2 = ((GoB (SpStSeq D)) * (len (GoB (SpStSeq D))),(width (GoB (SpStSeq D)))) `2 by A29, A46, A48, A62, GOBOARD2:def 1;
(S-max (L~ (SpStSeq D))) `2 = (Incr (Y_axis (SpStSeq D))) . 1 by A69, EUCLID:56;
then (S-max (L~ (SpStSeq D))) `2 = |[((Incr (X_axis (SpStSeq D))) . 2),((Incr (Y_axis (SpStSeq D))) . 1)]| `2 by EUCLID:56;
then A72: (S-max (L~ (SpStSeq D))) `2 = ((GoB (SpStSeq D)) * (len (GoB (SpStSeq D))),1) `2 by A29, A46, A59, GOBOARD2:def 1;
(N-max (L~ (SpStSeq D))) `1 = (NE-corner D) `1 by SPRECT_1:85
.= E-bound D by EUCLID:56
.= E-bound (L~ (SpStSeq D)) by SPRECT_1:69
.= (Incr (X_axis (SpStSeq D))) . 2 by A43, A36, A45, Th8 ;
then (N-max (L~ (SpStSeq D))) `1 = |[((Incr (X_axis (SpStSeq D))) . (1 + 1)),((Incr (Y_axis (SpStSeq D))) . (1 + 1))]| `1 by EUCLID:56;
then (N-max (L~ (SpStSeq D))) `1 = ((GoB (SpStSeq D)) * (len (GoB (SpStSeq D))),(width (GoB (SpStSeq D)))) `1 by A29, A46, A48, A62, GOBOARD2:def 1;
hence ( len (GoB (SpStSeq D)) = 2 & width (GoB (SpStSeq D)) = 2 & (SpStSeq D) /. 1 = (GoB (SpStSeq D)) * 1,2 & (SpStSeq D) /. 2 = (GoB (SpStSeq D)) * 2,2 & (SpStSeq D) /. 3 = (GoB (SpStSeq D)) * 2,1 & (SpStSeq D) /. 4 = (GoB (SpStSeq D)) * 1,1 & (SpStSeq D) /. 5 = (GoB (SpStSeq D)) * 1,2 ) by A11, A23, A9, A6, A14, A3, A46, A48, A63, A60, A61, A68, A71, A72, A70, A65, A64, EUCLID:57; :: thesis: verum