let f be V8() standard special_circular_sequence; ( not f /. 1 = N-min (L~ f) or f is clockwise_oriented or Rev f is clockwise_oriented )
assume A1:
f /. 1 = N-min (L~ f)
; ( f is clockwise_oriented or Rev f is clockwise_oriented )
(1 + 1) + 1 < len f
by GOBOARD7:34, XXREAL_0:2;
then A2:
2 < (len f) -' 1
by NAT_D:52;
A3:
width (GoB f) in NAT
;
A4:
[(i_w_n f),(width (GoB f))] in Indices (GoB f)
by JORDAN5D:def 7;
then A5:
i_w_n f <= len (GoB f)
by MATRIX_1:38;
A6:
1 <= width (GoB f)
by A4, MATRIX_1:38;
A7:
(GoB f) * ((i_w_n f),(width (GoB f))) = N-min (L~ f)
by JORDAN5D:def 7;
A8:
len f > 1 + 1
by GOBOARD7:34, XXREAL_0:2;
then A9:
1 + 1 in dom f
by FINSEQ_3:25;
then consider i1, j1 being Element of NAT such that
A10:
[i1,j1] in Indices (GoB f)
and
A11:
f /. 2 = (GoB f) * (i1,j1)
by GOBOARD5:11;
A12:
j1 <= width (GoB f)
by A10, MATRIX_1:38;
A13:
1 <= j1
by A10, MATRIX_1:38;
then A14:
1 <= width (GoB f)
by A12, XXREAL_0:2;
A15:
1 <= i1
by A10, MATRIX_1:38;
A16:
i1 <= len (GoB f)
by A10, MATRIX_1:38;
A17:
now assume A18:
width (GoB f) = j1
;
i_w_n f <= i1then
((GoB f) * (1,j1)) `2 = N-bound (L~ f)
by JORDAN5D:40;
then
((GoB f) * (i1,j1)) `2 = N-bound (L~ f)
by A13, A12, A15, A16, GOBOARD5:1;
then
(GoB f) * (
i1,
j1)
in N-most (L~ f)
by A8, A9, A11, GOBOARD1:1, SPRECT_2:10;
then
(N-min (L~ f)) `1 <= ((GoB f) * (i1,j1)) `1
by PSCOMP_1:39;
hence
i_w_n f <= i1
by A7, A13, A5, A15, A18, GOBOARD5:3;
verum end;
A19:
len f > 1
by GOBOARD7:34, XXREAL_0:2;
then A20:
len f in dom f
by FINSEQ_3:25;
1 in dom f
by A19, FINSEQ_3:25;
then
(abs ((i_w_n f) - i1)) + (abs ((width (GoB f)) - j1)) = 1
by A1, A4, A7, A9, A10, A11, GOBOARD5:12;
then
( ( abs ((i_w_n f) - i1) = 1 & width (GoB f) = j1 ) or ( abs ((width (GoB f)) - j1) = 1 & i_w_n f = i1 ) )
by SEQM_3:42;
then A21:
( ( i1 = (i_w_n f) + 1 & width (GoB f) = j1 ) or ( width (GoB f) = j1 + 1 & i_w_n f = i1 ) )
by A3, A12, A17, SEQM_3:41;
i_e_n f <= len (GoB f)
by JORDAN5D:45;
then
i_w_n f < len (GoB f)
by SPRECT_3:27, XXREAL_0:2;
then A22:
( 1 <= (i_w_n f) + 1 & (i_w_n f) + 1 <= len (GoB f) )
by NAT_1:11, NAT_1:13;
A23:
(len f) -' 1 <= len f
by NAT_D:44;
1 <= (len f) -' 1
by A8, NAT_D:55;
then A24:
(len f) -' 1 in dom f
by A23, FINSEQ_3:25;
then consider i2, j2 being Element of NAT such that
A25:
[i2,j2] in Indices (GoB f)
and
A26:
f /. ((len f) -' 1) = (GoB f) * (i2,j2)
by GOBOARD5:11;
A27:
j2 <= width (GoB f)
by A25, MATRIX_1:38;
A28:
1 <= i2
by A25, MATRIX_1:38;
A29:
( 1 <= j2 & i2 <= len (GoB f) )
by A25, MATRIX_1:38;
A30:
now assume A31:
width (GoB f) = j2
;
i_w_n f <= i2then
((GoB f) * (1,j2)) `2 = N-bound (L~ f)
by JORDAN5D:40;
then
((GoB f) * (i2,j2)) `2 = N-bound (L~ f)
by A27, A28, A29, GOBOARD5:1;
then
(GoB f) * (
i2,
j2)
in N-most (L~ f)
by A8, A24, A26, GOBOARD1:1, SPRECT_2:10;
then
(N-min (L~ f)) `1 <= ((GoB f) * (i2,j2)) `1
by PSCOMP_1:39;
hence
i_w_n f <= i2
by A7, A5, A28, A14, A31, GOBOARD5:3;
verum end;
A32:
len f > 4
by GOBOARD7:34;
then A33:
(GoB f) * (i2,j2) in L~ f
by A24, A26, GOBOARD1:1, XXREAL_0:2;
A34:
((len f) -' 1) + 1 = len f
by A32, XREAL_1:235, XXREAL_0:2;
then
f /. (((len f) -' 1) + 1) = f /. 1
by FINSEQ_6:def 1;
then
(abs (i2 - (i_w_n f))) + (abs (j2 - (width (GoB f)))) = 1
by A1, A24, A4, A7, A25, A26, A20, A34, GOBOARD5:12;
then
( ( abs (i2 - (i_w_n f)) = 1 & j2 = width (GoB f) ) or ( abs (j2 - (width (GoB f))) = 1 & i2 = i_w_n f ) )
by SEQM_3:42;
then
( ( i2 = (i_w_n f) + 1 & j2 = width (GoB f) ) or ( j2 + 1 = width (GoB f) & i2 = i_w_n f ) )
by A3, A27, A30, SEQM_3:41;
then
( (f /. 2) `2 = ((GoB f) * (1,(width (GoB f)))) `2 or (f /. ((len f) -' 1)) `2 = ((GoB f) * (1,(width (GoB f)))) `2 )
by A23, A11, A26, A6, A21, A22, A2, GOBOARD5:1, GOBOARD7:37;
then
( (f /. 2) `2 = N-bound (L~ f) or (f /. ((len f) -' 1)) `2 = N-bound (L~ f) )
by JORDAN5D:40;
then A35:
( f /. 2 in N-most (L~ f) or f /. ((len f) -' 1) in N-most (L~ f) )
by A8, A9, A26, A33, GOBOARD1:1, SPRECT_2:10;
reconsider A = L~ (Rev f) as non empty compact Subset of (TOP-REAL 2) ;
A36:
A = L~ f
by SPPOL_2:22;
((len f) -' 1) + (1 + 1) =
(((len f) -' 1) + 1) + 1
.=
(len f) + 1
by A32, XREAL_1:235, XXREAL_0:2
;
then A37:
(Rev f) /. 2 = f /. ((len f) -' 1)
by A24, FINSEQ_5:66;
(Rev f) /. 1 =
f /. (len f)
by FINSEQ_5:65
.=
N-min (L~ f)
by A1, FINSEQ_6:def 1
.=
N-min A
by SPPOL_2:22
;
hence
( f is clockwise_oriented or Rev f is clockwise_oriented )
by A1, A37, A36, A35, SPRECT_2:30; verum