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:32;
A2: len (SpStSeq D) = 5 by SPRECT_1:82;
then A3: (SpStSeq D) /. 5 = (SpStSeq D) /. 1 by FINSEQ_6:def 1;
4 in Seg (len (SpStSeq D)) by A2, FINSEQ_1:1;
then A4: 4 in dom (SpStSeq D) by FINSEQ_1:def 3;
then 4 in dom (X_axis (SpStSeq D)) by SPRECT_2:15;
then ( (SpStSeq D) /. 4 = W-min (L~ (SpStSeq D)) & (X_axis (SpStSeq D)) . 4 = ((SpStSeq D) /. 4) `1 ) by GOBOARD1:def 1, SPRECT_1:86;
then A5: (X_axis (SpStSeq D)) . 4 = W-bound (L~ (SpStSeq D)) ;
A6: (SpStSeq D) /. 3 = S-max (L~ (SpStSeq D)) by SPRECT_1:85;
3 in Seg (len (SpStSeq D)) by A2, FINSEQ_1:1;
then A7: 3 in dom (SpStSeq D) by FINSEQ_1:def 3;
then 3 in dom (X_axis (SpStSeq D)) by SPRECT_2:15;
then ( (SpStSeq D) /. 3 = E-min (L~ (SpStSeq D)) & (X_axis (SpStSeq D)) . 3 = ((SpStSeq D) /. 3) `1 ) by GOBOARD1:def 1, SPRECT_1:85;
then A8: (X_axis (SpStSeq D)) . 3 = E-bound (L~ (SpStSeq D)) ;
A9: (SpStSeq D) /. (1 + 1) = N-max (L~ (SpStSeq D)) by SPRECT_1:84;
3 in dom (Y_axis (SpStSeq D)) by A7, SPRECT_2:16;
then (Y_axis (SpStSeq D)) . 3 = ((SpStSeq D) /. 3) `2 by GOBOARD1:def 2;
then A10: (Y_axis (SpStSeq D)) . 3 = S-bound (L~ (SpStSeq D)) by A6;
A11: (SpStSeq D) /. 1 = N-min (L~ (SpStSeq D)) by SPRECT_1:83;
1 in Seg (len (SpStSeq D)) by A2, FINSEQ_1:1;
then A12: 1 in dom (SpStSeq D) by FINSEQ_1:def 3;
then 1 in dom (Y_axis (SpStSeq D)) by SPRECT_2:16;
then (Y_axis (SpStSeq D)) . 1 = ((SpStSeq D) /. 1) `2 by GOBOARD1:def 2;
then A13: (Y_axis (SpStSeq D)) . 1 = N-bound (L~ (SpStSeq D)) by A11;
A14: (SpStSeq D) /. 4 = S-min (L~ (SpStSeq D)) by SPRECT_1:86;
2 in Seg (len (SpStSeq D)) by A2, FINSEQ_1:1;
then A15: 2 in dom (SpStSeq D) by FINSEQ_1:def 3;
then 2 in dom (X_axis (SpStSeq D)) by SPRECT_2:15;
then ( (SpStSeq D) /. (1 + 1) = E-max (L~ (SpStSeq D)) & (X_axis (SpStSeq D)) . 2 = ((SpStSeq D) /. 2) `1 ) by GOBOARD1:def 1, SPRECT_1:84;
then A16: (X_axis (SpStSeq D)) . 2 = E-bound (L~ (SpStSeq D)) ;
4 in dom (Y_axis (SpStSeq D)) by A4, SPRECT_2:16;
then (Y_axis (SpStSeq D)) . 4 = ((SpStSeq D) /. 4) `2 by GOBOARD1:def 2;
then A17: (Y_axis (SpStSeq D)) . 4 = S-bound (L~ (SpStSeq D)) by A14;
2 in dom (Y_axis (SpStSeq D)) by A15, SPRECT_2:16;
then (Y_axis (SpStSeq D)) . 2 = ((SpStSeq D) /. 2) `2 by GOBOARD1:def 2;
then A18: (Y_axis (SpStSeq D)) . 2 = N-bound (L~ (SpStSeq D)) by A9;
A19: {(S-bound (L~ (SpStSeq D))),(N-bound (L~ (SpStSeq D)))} c= rng (Y_axis (SpStSeq D))

proof

let z be object ; :: 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 :: thesis: ( ( z = S-bound (L~ (SpStSeq D)) & z in rng (Y_axis (SpStSeq D)) ) or ( z = N-bound (L~ (SpStSeq D)) & z in rng (Y_axis (SpStSeq D)) ) )

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:16;
hence z in rng (Y_axis (SpStSeq D)) by A17, A21, FUNCT_1:def 3; :: 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:16;
hence z in rng (Y_axis (SpStSeq D)) by A18, A22, FUNCT_1:def 3; :: 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:83;
1 in dom (X_axis (SpStSeq D)) by A12, SPRECT_2:15;
then (X_axis (SpStSeq D)) . 1 = ((SpStSeq D) /. 1) `1 by GOBOARD1:def 1;
then A24: (X_axis (SpStSeq D)) . 1 = W-bound (L~ (SpStSeq D)) by A23;
A25: {(W-bound (L~ (SpStSeq D))),(E-bound (L~ (SpStSeq D)))} c= rng (X_axis (SpStSeq D))

proof

let z be object ; :: 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 :: thesis: ( ( z = W-bound (L~ (SpStSeq D)) & z in rng (X_axis (SpStSeq D)) ) or ( z = E-bound (L~ (SpStSeq D)) & z in rng (X_axis (SpStSeq D)) ) )

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:15;
hence z in rng (X_axis (SpStSeq D)) by A24, A27, FUNCT_1:def 3; :: 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:15;
hence z in rng (X_axis (SpStSeq D)) by A16, A28, FUNCT_1:def 3; :: 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 2;
5 in Seg (len (SpStSeq D)) by A2, FINSEQ_1:1;
then A30: 5 in dom (SpStSeq D) by FINSEQ_1:def 3;
then 5 in dom (X_axis (SpStSeq D)) by SPRECT_2:15;
then (X_axis (SpStSeq D)) . 5 = ((SpStSeq D) /. 5) `1 by GOBOARD1:def 1;
then A31: (X_axis (SpStSeq D)) . 5 = W-bound (L~ (SpStSeq D)) by A23, A3;
rng (X_axis (SpStSeq D)) c= {(W-bound (L~ (SpStSeq D))),(E-bound (L~ (SpStSeq D)))}

proof

let z be object ; :: 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 object such that
A32: u in dom (X_axis (SpStSeq D)) and
A33: z = (X_axis (SpStSeq D)) . u by FUNCT_1:def 3;
reconsider mu = u as Element of NAT by A32;
u in dom (SpStSeq D) by A32, SPRECT_2:15;
then u in Seg (len (SpStSeq D)) by FINSEQ_1:def 3;
then ( 1 <= mu & mu <= 5 ) by A2, FINSEQ_1:1;
then A34: 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 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;
then A36: rng (Incr (X_axis (SpStSeq D))) = {(W-bound (L~ (SpStSeq D))),(E-bound (L~ (SpStSeq D)))} by SEQ_4:def 21;
5 in dom (Y_axis (SpStSeq D)) by A30, SPRECT_2:16;
then (Y_axis (SpStSeq D)) . 5 = ((SpStSeq D) /. 5) `2 by GOBOARD1:def 2;
then A37: (Y_axis (SpStSeq D)) . 5 = N-bound (L~ (SpStSeq D)) by A11, A3;
rng (Y_axis (SpStSeq D)) c= {(S-bound (L~ (SpStSeq D))),(N-bound (L~ (SpStSeq D)))}

proof

let z be object ; :: 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 object such that
A38: u in dom (Y_axis (SpStSeq D)) and
A39: z = (Y_axis (SpStSeq D)) . u by FUNCT_1:def 3;
reconsider mu = u as Element of NAT by A38;
u in dom (SpStSeq D) by A38, SPRECT_2:16;
then u in Seg (len (SpStSeq D)) by FINSEQ_1:def 3;
then ( 1 <= mu & mu <= 5 ) by A2, FINSEQ_1:1;
then A40: 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 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;
then card (rng (Y_axis (SpStSeq D))) = 2 by A1, CARD_2:57;
then A42: len (Incr (Y_axis (SpStSeq D))) = 2 by SEQ_4:def 21;
A43: W-bound (L~ (SpStSeq D)) < E-bound (L~ (SpStSeq D)) by SPRECT_1:31;
then A44: card (rng (X_axis (SpStSeq D))) = 2 by A35, CARD_2:57;
then A45: len (Incr (X_axis (SpStSeq D))) = 2 by SEQ_4:def 21;
A46: len (GoB (SpStSeq D)) = card (rng (X_axis (SpStSeq D))) by GOBOARD2:13
.= 1 + 1 by A43, A35, CARD_2:57 ;
then A47: 1 in Seg (len (GoB (SpStSeq D))) by FINSEQ_1:1;
A48: width (GoB (SpStSeq D)) = card (rng (Y_axis (SpStSeq D))) by GOBOARD2:13
.= 1 + 1 by A1, A41, CARD_2:57 ;
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 21 ;
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_0:def 3;
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 object st x in rng (GoB (SpStSeq D)) holds
ex s being FinSequence st
( s = x & len s = n ) by MATRIX_0: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 2;
then ex s being FinSequence st
( s = s1 & len s = n ) by A51;
hence len p = 2 by A48, A50, A52, GOBOARD2:def 2; :: thesis: verum

end;

then A53: GoB (SpStSeq D) is Matrix of 2,2, the carrier of (TOP-REAL 2) by A46, MATRIX_0:def 2;
A54: 1 in Seg (width (GoB (SpStSeq D))) by A48, FINSEQ_1:1;
then [1,1] in [:(Seg (len (GoB (SpStSeq D)))),(Seg (width (GoB (SpStSeq D)))):] by A47, ZFMISC_1:87;
then A55: [1,1] in Indices (GoB (SpStSeq D)) by A46, A48, A53, MATRIX_0:24;
A56: width (GoB (SpStSeq D)) in Seg (width (GoB (SpStSeq D))) by A48, FINSEQ_1:1;
then [1,(width (GoB (SpStSeq D)))] in [:(Seg (len (GoB (SpStSeq D)))),(Seg (width (GoB (SpStSeq D)))):] by A47, ZFMISC_1:87;
then A57: [1,(width (GoB (SpStSeq D)))] in Indices (GoB (SpStSeq D)) by A46, A48, A53, MATRIX_0:24;
A58: len (GoB (SpStSeq D)) in Seg (len (GoB (SpStSeq D))) by A46, FINSEQ_1:1;
then [(len (GoB (SpStSeq D))),1] in [:(Seg (len (GoB (SpStSeq D)))),(Seg (width (GoB (SpStSeq D)))):] by A54, ZFMISC_1:87;
then A59: [(len (GoB (SpStSeq D))),1] in Indices (GoB (SpStSeq D)) by A46, A48, A53, MATRIX_0:24;
(S-max (L~ (SpStSeq D))) `1 = (SE-corner D) `1 by SPRECT_1:81
.= E-bound D
.= E-bound (L~ (SpStSeq D)) by SPRECT_1:61
.= (Incr (X_axis (SpStSeq D))) . 2 by A43, A36, A45, Th1 ;
then (S-max (L~ (SpStSeq D))) `1 = |[((Incr (X_axis (SpStSeq D))) . 2),((Incr (Y_axis (SpStSeq D))) . 1)]| `1 ;
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:80
.= W-bound D
.= W-bound (L~ (SpStSeq D)) by SPRECT_1:58
.= (Incr (X_axis (SpStSeq D))) . 1 by A43, A36, A45, Th1 ;
then (S-min (L~ (SpStSeq D))) `1 = |[((Incr (X_axis (SpStSeq D))) . 1),((Incr (Y_axis (SpStSeq D))) . 1)]| `1 ;
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:87;
then A62: [(len (GoB (SpStSeq D))),(width (GoB (SpStSeq D)))] in Indices (GoB (SpStSeq D)) by A46, A48, A53, MATRIX_0:24;
W-bound (L~ (SpStSeq D)) = (Incr (X_axis (SpStSeq D))) . 1 by A43, A36, A45, Th1;
then (W-max (L~ (SpStSeq D))) `1 = (Incr (X_axis (SpStSeq D))) . 1 ;
then (W-max (L~ (SpStSeq D))) `1 = |[((Incr (X_axis (SpStSeq D))) . 1),((Incr (Y_axis (SpStSeq D))) . (1 + 1))]| `1 ;
then A63: (W-max (L~ (SpStSeq D))) `1 = ((GoB (SpStSeq D)) * (1,(width (GoB (SpStSeq D))))) `1 by A29, A48, A57, GOBOARD2:def 1;
A66: rng (Incr (Y_axis (SpStSeq D))) = {(S-bound (L~ (SpStSeq D))),(N-bound (L~ (SpStSeq D)))} by A41, SEQ_4:def 21;
then A67: N-bound (L~ (SpStSeq D)) = (Incr (Y_axis (SpStSeq D))) . 2 by A1, A42, Th1;
then (N-min (L~ (SpStSeq D))) `2 = (Incr (Y_axis (SpStSeq D))) . 2 ;
then (N-min (L~ (SpStSeq D))) `2 = |[((Incr (X_axis (SpStSeq D))) . 1),((Incr (Y_axis (SpStSeq D))) . 2)]| `2 ;
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, Th1;
then (S-min (L~ (SpStSeq D))) `2 = (Incr (Y_axis (SpStSeq D))) . 1 ;
then (S-min (L~ (SpStSeq D))) `2 = |[((Incr (X_axis (SpStSeq D))) . 1),((Incr (Y_axis (SpStSeq D))) . 1)]| `2 ;
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 = |[((Incr (X_axis (SpStSeq D))) . 2),((Incr (Y_axis (SpStSeq D))) . 2)]| `2 by A67;
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;
then (S-max (L~ (SpStSeq D))) `2 = |[((Incr (X_axis (SpStSeq D))) . 2),((Incr (Y_axis (SpStSeq D))) . 1)]| `2 ;
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:77
.= E-bound D
.= E-bound (L~ (SpStSeq D)) by SPRECT_1:61
.= (Incr (X_axis (SpStSeq D))) . 2 by A43, A36, A45, Th1 ;
then (N-max (L~ (SpStSeq D))) `1 = |[((Incr (X_axis (SpStSeq D))) . (1 + 1)),((Incr (Y_axis (SpStSeq D))) . (1 + 1))]| `1 ;
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, EUCLID:53; :: thesis: verum