let f be non constant standard special_circular_sequence; :: thesis: ( f is clockwise_oriented iff (Rotate f,(E-max (L~ f))) /. 2 in E-most (L~ f) )
set r = Rotate f,(E-max (L~ f));
set j = i_n_e (Rotate f,(E-max (L~ f)));
set i = len (GoB (Rotate f,(E-max (L~ f))));
A1: ( 1 + 1 <= len (Rotate f,(E-max (L~ f))) & Rotate f,(E-max (L~ f)) is_sequence_on GoB (Rotate f,(E-max (L~ f))) ) by GOBOARD5:def 5, TOPREAL8:3;
A2: E-max (L~ f) in rng f by SPRECT_2:50;
then A3: (Rotate f,(E-max (L~ f))) /. 1 = E-max (L~ f) by FINSEQ_6:98;
A4: 2 <= len f by TOPREAL8:3;
thus ( f is clockwise_oriented implies (Rotate f,(E-max (L~ f))) /. 2 in E-most (L~ f) ) :: thesis: ( (Rotate f,(E-max (L~ f))) /. 2 in E-most (L~ f) implies f is clockwise_oriented )

proof

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

end;

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

now

assume east_halfline p meets L~ (Rotate f,(E-max (L~ f))) ; :: thesis: contradiction
then (east_halfline p) /\ (L~ (Rotate f,(E-max (L~ f)))) <> {} by XBOOLE_0:def 7;
then consider a being set such that
A45: a in (east_halfline p) /\ (L~ (Rotate f,(E-max (L~ f)))) by XBOOLE_0:def 1;
A46: a in L~ (Rotate f,(E-max (L~ f))) by A45, XBOOLE_0:def 4;
A47: a in east_halfline p by A45, XBOOLE_0:def 4;
reconsider a = a as Point of (TOP-REAL 2) by A45;
a `1 >= p `1 by A47, TOPREAL1:def 13;
then A48: a `1 >= t by A43, EUCLID:56;
((GoB (Rotate f,(E-max (L~ f)))) * (len (GoB (Rotate f,(E-max (L~ f))))),1) `1 = ((GoB (Rotate f,(E-max (L~ f)))) * (len (GoB (Rotate f,(E-max (L~ f))))),(i_n_e (Rotate f,(E-max (L~ f))))) `1 by A39, A25, A37, GOBOARD5:3;
then a `1 > ((GoB (Rotate f,(E-max (L~ f)))) * (len (GoB (Rotate f,(E-max (L~ f))))),(i_n_e (Rotate f,(E-max (L~ f))))) `1 by A44, A48, XXREAL_0:2;
then a `1 > E-bound (L~ (Rotate f,(E-max (L~ f)))) by A27, A3, A28, EUCLID:56;
hence contradiction by A46, PSCOMP_1:71; :: thesis: verum

end;

then A49: east_halfline p c= UBD (L~ (Rotate f,(E-max (L~ f)))) by JORDAN2C:135;
p in east_halfline p by TOPREAL1:45;
then LeftComp (Rotate f,(E-max (L~ f))) meets UBD (L~ (Rotate f,(E-max (L~ f)))) by A33, A34, A49, XBOOLE_0:3;
then Rotate f,(E-max (L~ f)) is clockwise_oriented by A35, GOBOARD9:3, JORDAN1H:49;
hence f is clockwise_oriented by JORDAN1H:48; :: thesis: verum