let f be non constant standard special_circular_sequence; :: thesis: ( f is clockwise_oriented iff (Rotate f,(W-min (L~ f))) /. 2 in W-most (L~ f) )
set r = Rotate f,(W-min (L~ f));
A1: L~ (Rotate f,(W-min (L~ f))) = L~ f by REVROT_1:33;
A2: W-min (L~ f) in rng f by SPRECT_2:47;
then A3: (Rotate f,(W-min (L~ f))) /. 1 = W-min (L~ f) by FINSEQ_6:98;
A4: 1 + 1 <= len (Rotate f,(W-min (L~ f))) by TOPREAL8:3;
A5: 2 <= len f by TOPREAL8:3;
rng (Rotate f,(W-min (L~ f))) = rng f by FINSEQ_6:96, SPRECT_2:47;
then A6: 1 in dom (Rotate f,(W-min (L~ f))) by FINSEQ_3:33, SPRECT_2:47;
A7: Rotate f,(W-min (L~ f)) is_sequence_on GoB (Rotate f,(W-min (L~ f))) by GOBOARD5:def 5;
set j = i_s_w (Rotate f,(W-min (L~ f)));
set i = 1;
A8: ( [1,(i_s_w (Rotate f,(W-min (L~ f))))] in Indices (GoB (Rotate f,(W-min (L~ f)))) & (GoB (Rotate f,(W-min (L~ f)))) * 1,(i_s_w (Rotate f,(W-min (L~ f)))) = (Rotate f,(W-min (L~ f))) /. 1 ) by A1, A3, JORDAN5D:def 1;
then A9: ( 1 <= 1 & 1 <= len (GoB (Rotate f,(W-min (L~ f)))) & 1 <= i_s_w (Rotate f,(W-min (L~ f))) & i_s_w (Rotate f,(W-min (L~ f))) <= width (GoB (Rotate f,(W-min (L~ f)))) ) by MATRIX_1:39;
A10: 1 -' 1 = 1 - 1 by XREAL_1:235;
thus ( f is clockwise_oriented implies (Rotate f,(W-min (L~ f))) /. 2 in W-most (L~ f) ) :: thesis: ( (Rotate f,(W-min (L~ f))) /. 2 in W-most (L~ f) implies f is clockwise_oriented )

proof

assume A11: f is clockwise_oriented ; :: thesis: (Rotate f,(W-min (L~ f))) /. 2 in W-most (L~ f)
set k = (W-min (L~ f)) .. f;
(W-min (L~ f)) .. f < len f by SPRECT_5:21;
then A12: ( 1 <= (W-min (L~ f)) .. f & ((W-min (L~ f)) .. f) + 1 <= len f ) by A2, FINSEQ_4:31, NAT_1:13;
A13: f /. ((W-min (L~ f)) .. f) = W-min (L~ f) by A2, FINSEQ_5:41;
f is_sequence_on GoB f by GOBOARD5:def 5;
then f is_sequence_on GoB (Rotate f,(W-min (L~ f))) by REVROT_1:28;
then consider i, j being Element of NAT such that
A14: ( [i,j] in Indices (GoB (Rotate f,(W-min (L~ f)))) & [i,(j + 1)] in Indices (GoB (Rotate f,(W-min (L~ f)))) & f /. ((W-min (L~ f)) .. f) = (GoB (Rotate f,(W-min (L~ f)))) * i,j & f /. (((W-min (L~ f)) .. f) + 1) = (GoB (Rotate f,(W-min (L~ f)))) * i,(j + 1) ) by A11, A12, A13, Th23;
A15: ( 1 <= i & i <= len (GoB (Rotate f,(W-min (L~ f)))) & 1 <= j & j <= width (GoB (Rotate f,(W-min (L~ f)))) ) by A14, MATRIX_1:39;
A16: ( 1 <= i & i <= len (GoB (Rotate f,(W-min (L~ f)))) & 1 <= j + 1 & j + 1 <= width (GoB (Rotate f,(W-min (L~ f)))) ) by A14, MATRIX_1:39;
(W-min (L~ f)) .. f <= ((W-min (L~ f)) .. f) + 1 by NAT_1:13;
then A17: f /. (((W-min (L~ f)) .. f) + 1) = (Rotate f,(W-min (L~ f))) /. (((((W-min (L~ f)) .. f) + 1) + 1) -' ((W-min (L~ f)) .. f)) by A2, A12, REVROT_1:10
.= (Rotate f,(W-min (L~ f))) /. ((((W-min (L~ f)) .. f) + (1 + 1)) -' ((W-min (L~ f)) .. f))
.= (Rotate f,(W-min (L~ f))) /. 2 by NAT_D:34 ;
1 <= ((W-min (L~ f)) .. f) + 1 by NAT_1:11;
then ((W-min (L~ f)) .. f) + 1 in dom f by A12, FINSEQ_3:27;
then ( ((W-min (L~ f)) .. f) + 1 in dom f & f /. (((W-min (L~ f)) .. f) + 1) = f . (((W-min (L~ f)) .. f) + 1) ) by PARTFUN1:def 8;
then A18: f /. (((W-min (L~ f)) .. f) + 1) in rng f by FUNCT_1:12;
A19: rng f c= L~ f by A5, SPPOL_2:18;
(f /. (((W-min (L~ f)) .. f) + 1)) `1 = ((GoB (Rotate f,(W-min (L~ f)))) * i,1) `1 by A14, A16, GOBOARD5:3
.= (f /. ((W-min (L~ f)) .. f)) `1 by A14, A15, GOBOARD5:3
.= W-bound (L~ f) by A13, EUCLID:56 ;
hence (Rotate f,(W-min (L~ f))) /. 2 in W-most (L~ f) by A17, A18, A19, SPRECT_2:16; :: thesis: verum

end;

assume A20: (Rotate f,(W-min (L~ f))) /. 2 in W-most (L~ f) ; :: thesis: f is clockwise_oriented
len (Rotate f,(W-min (L~ f))) > 2 by TOPREAL8:3;
then A21: 1 + 1 in dom (Rotate f,(W-min (L~ f))) by FINSEQ_3:27;
then consider i2, j2 being Element of NAT such that
A22: ( [i2,j2] in Indices (GoB (Rotate f,(W-min (L~ f)))) & (Rotate f,(W-min (L~ f))) /. (1 + 1) = (GoB (Rotate f,(W-min (L~ f)))) * i2,j2 ) by A7, GOBOARD1:def 11;
A23: ( ((GoB (Rotate f,(W-min (L~ f)))) * i2,j2) `1 = ((GoB (Rotate f,(W-min (L~ f)))) * 1,(i_s_w (Rotate f,(W-min (L~ f))))) `1 & ((GoB (Rotate f,(W-min (L~ f)))) * 1,(i_s_w (Rotate f,(W-min (L~ f))))) `2 <= ((GoB (Rotate f,(W-min (L~ f)))) * i2,j2) `2 ) by A3, A8, A20, A22, PSCOMP_1:88;
then A24: i2 = 1 by A8, A22, JORDAN1G:7;
then (abs (1 - 1)) + (abs ((i_s_w (Rotate f,(W-min (L~ f)))) - j2)) = 1 by A6, A7, A8, A21, A22, GOBOARD1:def 11;
then 0 + (abs ((i_s_w (Rotate f,(W-min (L~ f)))) - j2)) = 1 by ABSVALUE:7;
then A25: abs (j2 - (i_s_w (Rotate f,(W-min (L~ f))))) = 1 by UNIFORM1:13;
1 <= j2 by A22, MATRIX_1:39;
then j2 - (i_s_w (Rotate f,(W-min (L~ f)))) >= 0 by A9, A23, A24, GOBOARD5:5, XREAL_1:50;
then A26: j2 - (i_s_w (Rotate f,(W-min (L~ f)))) = 1 by A25, ABSVALUE:def 1;
then A27: j2 = (i_s_w (Rotate f,(W-min (L~ f)))) + 1 ;
(i_s_w (Rotate f,(W-min (L~ f)))) + 1 <= width (GoB (Rotate f,(W-min (L~ f)))) by A22, A26, MATRIX_1:39;
then A28: i_s_w (Rotate f,(W-min (L~ f))) < width (GoB (Rotate f,(W-min (L~ f)))) by NAT_1:13;
left_cell (Rotate f,(W-min (L~ f))),1,(GoB (Rotate f,(W-min (L~ f)))) = cell (GoB (Rotate f,(W-min (L~ f)))),(1 -' 1),(i_s_w (Rotate f,(W-min (L~ f)))) by A4, A7, A8, A22, A24, A27, GOBRD13:22;
then left_cell (Rotate f,(W-min (L~ f))),1 = cell (GoB (Rotate f,(W-min (L~ f)))),0 ,(i_s_w (Rotate f,(W-min (L~ f)))) by A4, A10, JORDAN1H:27;
then A29: Int (left_cell (Rotate f,(W-min (L~ f))),1) = { |[t,s]| where t, s is Real : ( t < ((GoB (Rotate f,(W-min (L~ f)))) * 1,1) `1 & ((GoB (Rotate f,(W-min (L~ f)))) * 1,(i_s_w (Rotate f,(W-min (L~ f))))) `2 < s & s < ((GoB (Rotate f,(W-min (L~ f)))) * 1,((i_s_w (Rotate f,(W-min (L~ f)))) + 1)) `2 ) } by A9, A28, GOBOARD6:23;
A30: Int (left_cell (Rotate f,(W-min (L~ f))),1) c= LeftComp (Rotate f,(W-min (L~ f))) by A4, GOBOARD9:24;
Int (left_cell (Rotate f,(W-min (L~ f))),1) <> {} by A4, GOBOARD9:18;
then consider p being set such that
A31: p in Int (left_cell (Rotate f,(W-min (L~ f))),1) by XBOOLE_0:def 1;
reconsider p = p as Point of (TOP-REAL 2) by A31;
consider t, s being Real such that
A32: ( p = |[t,s]| & t < ((GoB (Rotate f,(W-min (L~ f)))) * 1,1) `1 & ((GoB (Rotate f,(W-min (L~ f)))) * 1,(i_s_w (Rotate f,(W-min (L~ f))))) `2 < s & s < ((GoB (Rotate f,(W-min (L~ f)))) * 1,((i_s_w (Rotate f,(W-min (L~ f)))) + 1)) `2 ) by A29, A31;

now

assume west_halfline p meets L~ (Rotate f,(W-min (L~ f))) ; :: thesis: contradiction
then (west_halfline p) /\ (L~ (Rotate f,(W-min (L~ f)))) <> {} by XBOOLE_0:def 7;
then consider a being set such that
A33: a in (west_halfline p) /\ (L~ (Rotate f,(W-min (L~ f)))) by XBOOLE_0:def 1;
A34: ( a in west_halfline p & a in L~ (Rotate f,(W-min (L~ f))) ) by A33, XBOOLE_0:def 4;
reconsider a = a as Point of (TOP-REAL 2) by A33;
A35: ((GoB (Rotate f,(W-min (L~ f)))) * 1,(i_s_w (Rotate f,(W-min (L~ f))))) `1 = ((GoB (Rotate f,(W-min (L~ f)))) * 1,1) `1 by A9, GOBOARD5:3;
a `1 <= p `1 by A34, TOPREAL1:def 15;
then a `1 <= t by A32, EUCLID:56;
then a `1 < ((GoB (Rotate f,(W-min (L~ f)))) * 1,(i_s_w (Rotate f,(W-min (L~ f))))) `1 by A32, A35, XXREAL_0:2;
then a `1 < W-bound (L~ (Rotate f,(W-min (L~ f)))) by A1, A3, A8, EUCLID:56;
hence contradiction by A34, PSCOMP_1:71; :: thesis: verum

end;

then A36: west_halfline p c= UBD (L~ (Rotate f,(W-min (L~ f)))) by JORDAN2C:134;
p in west_halfline p by TOPREAL1:45;
then A37: LeftComp (Rotate f,(W-min (L~ f))) meets UBD (L~ (Rotate f,(W-min (L~ f)))) by A30, A31, A36, XBOOLE_0:3;
A38: LeftComp (Rotate f,(W-min (L~ f))) is_a_component_of (L~ (Rotate f,(W-min (L~ f)))) ` by GOBOARD9:def 1;
UBD (L~ (Rotate f,(W-min (L~ f)))) is_a_component_of (L~ (Rotate f,(W-min (L~ f)))) ` by JORDAN2C:132;
then LeftComp (Rotate f,(W-min (L~ f))) = UBD (L~ (Rotate f,(W-min (L~ f)))) by A37, A38, GOBOARD9:3;
then Rotate f,(W-min (L~ f)) is clockwise_oriented by A37, A38, JORDAN1H:49;
hence f is clockwise_oriented by JORDAN1H:48; :: thesis: verum