set j = 1;
let f be non constant standard special_circular_sequence; :: thesis: ( f is clockwise_oriented iff (Rotate f,(S-max (L~ f))) /. 2 in S-most (L~ f) )
set r = Rotate f,(S-max (L~ f));
A1: Rotate f,(S-max (L~ f)) is_sequence_on GoB (Rotate f,(S-max (L~ f))) by GOBOARD5:def 5;
len (Rotate f,(S-max (L~ f))) > 2 by TOPREAL8:3;
then A2: 1 + 1 in dom (Rotate f,(S-max (L~ f))) by FINSEQ_3:27;
then consider i2, j2 being Element of NAT such that
A3: [i2,j2] in Indices (GoB (Rotate f,(S-max (L~ f)))) and
A4: (Rotate f,(S-max (L~ f))) /. (1 + 1) = (GoB (Rotate f,(S-max (L~ f)))) * i2,j2 by A1, GOBOARD1:def 11;
A5: i2 <= len (GoB (Rotate f,(S-max (L~ f)))) by A3, MATRIX_1:39;
set i = i_e_s (Rotate f,(S-max (L~ f)));
A6: S-max (L~ f) in rng f by SPRECT_2:46;
then A7: (Rotate f,(S-max (L~ f))) /. 1 = S-max (L~ f) by FINSEQ_6:98;
A8: 2 <= len f by TOPREAL8:3;
thus ( f is clockwise_oriented implies (Rotate f,(S-max (L~ f))) /. 2 in S-most (L~ f) ) :: thesis: ( (Rotate f,(S-max (L~ f))) /. 2 in S-most (L~ f) implies f is clockwise_oriented )

proof

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

end;

assume A23: (Rotate f,(S-max (L~ f))) /. 2 in S-most (L~ f) ; :: thesis: f is clockwise_oriented
A24: [(i_e_s (Rotate f,(S-max (L~ f)))),1] in Indices (GoB (Rotate f,(S-max (L~ f)))) by JORDAN5D:def 6;
then A25: 1 <= i_e_s (Rotate f,(S-max (L~ f))) by MATRIX_1:39;
A26: L~ (Rotate f,(S-max (L~ f))) = L~ f by REVROT_1:33;
then A27: (GoB (Rotate f,(S-max (L~ f)))) * (i_e_s (Rotate f,(S-max (L~ f)))),1 = (Rotate f,(S-max (L~ f))) /. 1 by A7, JORDAN5D:def 6;
then ((GoB (Rotate f,(S-max (L~ f)))) * (i_e_s (Rotate f,(S-max (L~ f)))),1) `2 = S-bound (L~ f) by A7, EUCLID:56
.= (S-min (L~ f)) `2 by EUCLID:56 ;
then ((GoB (Rotate f,(S-max (L~ f)))) * i2,j2) `2 = ((GoB (Rotate f,(S-max (L~ f)))) * (i_e_s (Rotate f,(S-max (L~ f)))),1) `2 by A23, A4, PSCOMP_1:118;
then A28: j2 = 1 by A24, A3, JORDAN1G:6;
A29: 1 <= width (GoB (Rotate f,(S-max (L~ f)))) by A24, MATRIX_1:39;
rng (Rotate f,(S-max (L~ f))) = rng f by FINSEQ_6:96, SPRECT_2:46;
then 1 in dom (Rotate f,(S-max (L~ f))) by FINSEQ_3:33, SPRECT_2:46;
then (abs (1 - 1)) + (abs ((i_e_s (Rotate f,(S-max (L~ f)))) - i2)) = 1 by A1, A24, A27, A2, A3, A4, A28, GOBOARD1:def 11;
then A30: 0 + (abs ((i_e_s (Rotate f,(S-max (L~ f)))) - i2)) = 1 by ABSVALUE:7;
((GoB (Rotate f,(S-max (L~ f)))) * i2,j2) `1 <= ((GoB (Rotate f,(S-max (L~ f)))) * (i_e_s (Rotate f,(S-max (L~ f)))),1) `1 by A7, A27, A23, A4, PSCOMP_1:118;
then (i_e_s (Rotate f,(S-max (L~ f)))) - i2 >= 0 by A25, A29, A28, A5, GOBOARD5:4, XREAL_1:50;
then A31: (i_e_s (Rotate f,(S-max (L~ f)))) - i2 = 1 by A30, ABSVALUE:def 1;
then i2 = (i_e_s (Rotate f,(S-max (L~ f)))) - 1 ;
then A32: i2 = (i_e_s (Rotate f,(S-max (L~ f)))) -' 1 by A25, XREAL_1:235;
then A33: 1 <= (i_e_s (Rotate f,(S-max (L~ f)))) -' 1 by A3, MATRIX_1:39;
A34: i_e_s (Rotate f,(S-max (L~ f))) <= len (GoB (Rotate f,(S-max (L~ f)))) by A24, MATRIX_1:39;
A35: 1 + 1 <= len (Rotate f,(S-max (L~ f))) by TOPREAL8:3;
then A36: Int (left_cell (Rotate f,(S-max (L~ f))),1) c= LeftComp (Rotate f,(S-max (L~ f))) by GOBOARD9:24;
Int (left_cell (Rotate f,(S-max (L~ f))),1) <> {} by A35, GOBOARD9:18;
then consider p being set such that
A37: p in Int (left_cell (Rotate f,(S-max (L~ f))),1) by XBOOLE_0:def 1;
[(((i_e_s (Rotate f,(S-max (L~ f)))) -' 1) + 1),1] in Indices (GoB (Rotate f,(S-max (L~ f)))) by A24, A25, XREAL_1:237;
then ( 1 -' 1 = 1 - 1 & left_cell (Rotate f,(S-max (L~ f))),1,(GoB (Rotate f,(S-max (L~ f)))) = cell (GoB (Rotate f,(S-max (L~ f)))),((i_e_s (Rotate f,(S-max (L~ f)))) -' 1),(1 -' 1) ) by A35, A1, A27, A3, A4, A28, A31, A32, GOBRD13:26, XREAL_1:235;
then A38: left_cell (Rotate f,(S-max (L~ f))),1 = cell (GoB (Rotate f,(S-max (L~ f)))),((i_e_s (Rotate f,(S-max (L~ f)))) -' 1),0 by A35, JORDAN1H:27;
(i_e_s (Rotate f,(S-max (L~ f)))) - 1 < i_e_s (Rotate f,(S-max (L~ f))) by XREAL_1:148;
then (i_e_s (Rotate f,(S-max (L~ f)))) -' 1 < len (GoB (Rotate f,(S-max (L~ f)))) by A34, A31, A32, XXREAL_0:2;
then A39: Int (left_cell (Rotate f,(S-max (L~ f))),1) = { |[t,s]| where t, s is Real : ( ((GoB (Rotate f,(S-max (L~ f)))) * ((i_e_s (Rotate f,(S-max (L~ f)))) -' 1),1) `1 < t & t < ((GoB (Rotate f,(S-max (L~ f)))) * (((i_e_s (Rotate f,(S-max (L~ f)))) -' 1) + 1),1) `1 & s < ((GoB (Rotate f,(S-max (L~ f)))) * 1,1) `2 ) } by A33, A38, GOBOARD6:27;
reconsider p = p as Point of (TOP-REAL 2) by A37;
A40: ( LeftComp (Rotate f,(S-max (L~ f))) is_a_component_of (L~ (Rotate f,(S-max (L~ f)))) ` & UBD (L~ (Rotate f,(S-max (L~ f)))) is_a_component_of (L~ (Rotate f,(S-max (L~ f)))) ` ) by GOBOARD9:def 1, JORDAN2C:132;
consider t, s being Real such that
A41: p = |[t,s]| and
((GoB (Rotate f,(S-max (L~ f)))) * ((i_e_s (Rotate f,(S-max (L~ f)))) -' 1),1) `1 < t and
t < ((GoB (Rotate f,(S-max (L~ f)))) * (((i_e_s (Rotate f,(S-max (L~ f)))) -' 1) + 1),1) `1 and
A42: s < ((GoB (Rotate f,(S-max (L~ f)))) * 1,1) `2 by A39, A37;

now

assume south_halfline p meets L~ (Rotate f,(S-max (L~ f))) ; :: thesis: contradiction
then (south_halfline p) /\ (L~ (Rotate f,(S-max (L~ f)))) <> {} by XBOOLE_0:def 7;
then consider a being set such that
A43: a in (south_halfline p) /\ (L~ (Rotate f,(S-max (L~ f)))) by XBOOLE_0:def 1;
A44: a in L~ (Rotate f,(S-max (L~ f))) by A43, XBOOLE_0:def 4;
A45: a in south_halfline p by A43, XBOOLE_0:def 4;
reconsider a = a as Point of (TOP-REAL 2) by A43;
a `2 <= p `2 by A45, TOPREAL1:def 14;
then a `2 <= s by A41, EUCLID:56;
then A46: a `2 < ((GoB (Rotate f,(S-max (L~ f)))) * 1,1) `2 by A42, XXREAL_0:2;
((GoB (Rotate f,(S-max (L~ f)))) * (i_e_s (Rotate f,(S-max (L~ f)))),1) `2 = ((GoB (Rotate f,(S-max (L~ f)))) * 1,1) `2 by A25, A34, A29, GOBOARD5:2;
then a `2 < S-bound (L~ (Rotate f,(S-max (L~ f)))) by A26, A7, A27, A46, EUCLID:56;
hence contradiction by A44, PSCOMP_1:71; :: thesis: verum

end;

then A47: south_halfline p c= UBD (L~ (Rotate f,(S-max (L~ f)))) by JORDAN2C:136;
p in south_halfline p by TOPREAL1:45;
then LeftComp (Rotate f,(S-max (L~ f))) meets UBD (L~ (Rotate f,(S-max (L~ f)))) by A36, A37, A47, XBOOLE_0:3;
then Rotate f,(S-max (L~ f)) is clockwise_oriented by A40, GOBOARD9:3, JORDAN1H:49;
hence f is clockwise_oriented by JORDAN1H:48; :: thesis: verum