let f be constant standard special_circular_sequence; :: thesis: ( 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) ; :: thesis: ( 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: [(i_w_n f),(width (GoB f))] in Indices (GoB f) by JORDAN5D:def 7;
then A4: i_w_n f <= len (GoB f) by MATRIX_0:32;
A5: 1 <= width (GoB f) by A3, MATRIX_0:32;
A6: (GoB f) * ((i_w_n f),(width (GoB f))) = N-min (L~ f) by JORDAN5D:def 7;
A7: len f > 1 + 1 by GOBOARD7:34, XXREAL_0:2;
then A8: 1 + 1 in dom f by FINSEQ_3:25;
then consider i1, j1 being Nat such that
A9: [i1,j1] in Indices (GoB f) and
A10: f /. 2 = (GoB f) * (i1,j1) by GOBOARD5:11;
A11: j1 <= width (GoB f) by A9, MATRIX_0:32;
A12: 1 <= j1 by A9, MATRIX_0:32;
then A13: 1 <= width (GoB f) by A11, XXREAL_0:2;
A14: 1 <= i1 by A9, MATRIX_0:32;
A15: i1 <= len (GoB f) by A9, MATRIX_0:32;

A16: now :: thesis: ( width (GoB f) = j1 implies i_w_n f <= i1 )

assume A17: width (GoB f) = j1 ; :: thesis: i_w_n f <= i1
then ((GoB f) * (1,j1)) `2 = N-bound (L~ f) by JORDAN5D:40;
then ((GoB f) * (i1,j1)) `2 = N-bound (L~ f) by A12, A11, A14, A15, GOBOARD5:1;
then (GoB f) * (i1,j1) in N-most (L~ f) by A7, A8, A10, 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 A6, A12, A4, A14, A17, GOBOARD5:3; :: thesis: verum

end;

A18: len f > 1 by GOBOARD7:34, XXREAL_0:2;
then A19: len f in dom f by FINSEQ_3:25;
1 in dom f by A18, FINSEQ_3:25;
then |.((i_w_n f) - i1).| + |.((width (GoB f)) - j1).| = 1 by A1, A3, A6, A8, A9, A10, GOBOARD5:12;
then ( ( |.((i_w_n f) - i1).| = 1 & width (GoB f) = j1 ) or ( |.((width (GoB f)) - j1).| = 1 & i_w_n f = i1 ) ) by SEQM_3:42;
then A20: ( ( i1 = (i_w_n f) + 1 & width (GoB f) = j1 ) or ( width (GoB f) = j1 + 1 & i_w_n f = i1 ) ) by A11, A16, 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 A21: ( 1 <= (i_w_n f) + 1 & (i_w_n f) + 1 <= len (GoB f) ) by NAT_1:11, NAT_1:13;
A22: (len f) -' 1 <= len f by NAT_D:44;
1 <= (len f) -' 1 by A7, NAT_D:55;
then A23: (len f) -' 1 in dom f by A22, FINSEQ_3:25;
then consider i2, j2 being Nat such that
A24: [i2,j2] in Indices (GoB f) and
A25: f /. ((len f) -' 1) = (GoB f) * (i2,j2) by GOBOARD5:11;
A26: j2 <= width (GoB f) by A24, MATRIX_0:32;
A27: 1 <= i2 by A24, MATRIX_0:32;
A28: ( 1 <= j2 & i2 <= len (GoB f) ) by A24, MATRIX_0:32;

A29: now :: thesis: ( width (GoB f) = j2 implies i_w_n f <= i2 )

assume A30: width (GoB f) = j2 ; :: thesis: i_w_n f <= i2
then ((GoB f) * (1,j2)) `2 = N-bound (L~ f) by JORDAN5D:40;
then ((GoB f) * (i2,j2)) `2 = N-bound (L~ f) by A26, A27, A28, GOBOARD5:1;
then (GoB f) * (i2,j2) in N-most (L~ f) by A7, A23, A25, 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 A6, A4, A27, A13, A30, GOBOARD5:3; :: thesis: verum

end;

A31: len f > 4 by GOBOARD7:34;
then A32: (GoB f) * (i2,j2) in L~ f by A23, A25, GOBOARD1:1, XXREAL_0:2;
A33: ((len f) -' 1) + 1 = len f by A31, XREAL_1:235, XXREAL_0:2;
then f /. (((len f) -' 1) + 1) = f /. 1 by FINSEQ_6:def 1;
then |.(i2 - (i_w_n f)).| + |.(j2 - (width (GoB f))).| = 1 by A1, A23, A3, A6, A24, A25, A19, A33, GOBOARD5:12;
then ( ( |.(i2 - (i_w_n f)).| = 1 & j2 = width (GoB f) ) or ( |.(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 A26, A29, 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 A22, A10, A25, A5, A20, A21, 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 A34: ( f /. 2 in N-most (L~ f) or f /. ((len f) -' 1) in N-most (L~ f) ) by A7, A8, A25, A32, GOBOARD1:1, SPRECT_2:10;
reconsider A = L~ (Rev f) as non empty compact Subset of (TOP-REAL 2) ;
A35: A = L~ f by SPPOL_2:22;
((len f) -' 1) + (1 + 1) = (((len f) -' 1) + 1) + 1
.= (len f) + 1 by A31, XREAL_1:235, XXREAL_0:2 ;
then A36: (Rev f) /. 2 = f /. ((len f) -' 1) by A23, 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, A36, A35, A34, SPRECT_2:30; :: thesis: verum