let f be V22() 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:46;

then A3: (Rotate (f,(E-max (L~ f)))) /. 1 = E-max (L~ f) by FINSEQ_6:92;

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 )

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:25, GOBOARD5:def 5;

then consider i2, j2 being 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 9;

A23: j2 <= width (GoB (Rotate (f,(E-max (L~ f))))) by A21, MATRIX_0:32;

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_0:32;

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:235;

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:235;

(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:50;

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:47;

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:47;

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:21;

Int (left_cell ((Rotate (f,(E-max (L~ f)))),1)) <> {} by A32, GOBOARD9:15;

then consider p being object 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:124;

A36: 1 <= j2 by A21, MATRIX_0:32;

A37: i_n_e (Rotate (f,(E-max (L~ f)))) <= width (GoB (Rotate (f,(E-max (L~ f))))) by A24, MATRIX_0:32;

rng (Rotate (f,(E-max (L~ f)))) = rng f by FINSEQ_6:90, SPRECT_2:46;

then 1 in dom (Rotate (f,(E-max (L~ f)))) by FINSEQ_3:31, SPRECT_2:46;

then |.(i2 - i2).| + |.((i_n_e (Rotate (f,(E-max (L~ f))))) - j2).| = 1 by A24, A28, A20, A21, A22, A31, GOBOARD1:def 9;

then A38: 0 + |.((i_n_e (Rotate (f,(E-max (L~ f))))) - j2).| = 1 by ABSVALUE:2;

A39: 1 <= len (GoB (Rotate (f,(E-max (L~ f))))) by A24, MATRIX_0:32;

((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:47;

then (i_n_e (Rotate (f,(E-max (L~ f))))) - j2 >= 0 by A39, A25, A31, A23, GOBOARD5:4, XREAL_1:48;

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:233;

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:27;

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:21;

(i_n_e (Rotate (f,(E-max (L~ f))))) - 1 < (i_n_e (Rotate (f,(E-max (L~ f))))) - 0 by XREAL_1:15;

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:23;

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;

p in east_halfline p by TOPREAL1:38;

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:1, JORDAN1H:41;

hence f is clockwise_oriented by JORDAN1H:40; :: thesis: verum

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:46;

then A3: (Rotate (f,(E-max (L~ f)))) /. 1 = E-max (L~ f) by FINSEQ_6:92;

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

assume A19:
(Rotate (f,(E-max (L~ f)))) /. 2 in E-most (L~ f)
; :: thesis: f is clockwise_oriented
set k = (E-max (L~ f)) .. f;

(E-max (L~ f)) .. f < len f by SPRECT_5:16;

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:25;

then f /. (((E-max (L~ f)) .. f) + 1) = f . (((E-max (L~ f)) .. f) + 1) by PARTFUN1:def 6;

then A7: f /. (((E-max (L~ f)) .. f) + 1) in rng f by A6, FUNCT_1:3;

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:38;

(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, FINSEQ_6:175

.= (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 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, Th23, FINSEQ_4:21;

A16: ( 1 <= j & j <= width (GoB (Rotate (f,(E-max (L~ f))))) ) by A13, MATRIX_0:32;

A17: ( 1 <= j + 1 & j + 1 <= width (GoB (Rotate (f,(E-max (L~ f))))) ) by A12, MATRIX_0:32;

A18: ( 1 <= i & i <= len (GoB (Rotate (f,(E-max (L~ f))))) ) by A12, MATRIX_0:32;

( 1 <= i & i <= len (GoB (Rotate (f,(E-max (L~ f))))) ) by A12, MATRIX_0:32;

then (f /. (((E-max (L~ f)) .. f) + 1)) `1 = ((GoB (Rotate (f,(E-max (L~ f))))) * (i,1)) `1 by A15, A16, GOBOARD5:2

.= (f /. ((E-max (L~ f)) .. f)) `1 by A14, A18, A17, GOBOARD5:2

.= E-bound (L~ f) by A9, EUCLID:52 ;

hence (Rotate (f,(E-max (L~ f)))) /. 2 in E-most (L~ f) by A10, A7, A8, SPRECT_2:13; :: thesis: verum

end;(E-max (L~ f)) .. f < len f by SPRECT_5:16;

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:25;

then f /. (((E-max (L~ f)) .. f) + 1) = f . (((E-max (L~ f)) .. f) + 1) by PARTFUN1:def 6;

then A7: f /. (((E-max (L~ f)) .. f) + 1) in rng f by A6, FUNCT_1:3;

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:38;

(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, FINSEQ_6:175

.= (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 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, Th23, FINSEQ_4:21;

A16: ( 1 <= j & j <= width (GoB (Rotate (f,(E-max (L~ f))))) ) by A13, MATRIX_0:32;

A17: ( 1 <= j + 1 & j + 1 <= width (GoB (Rotate (f,(E-max (L~ f))))) ) by A12, MATRIX_0:32;

A18: ( 1 <= i & i <= len (GoB (Rotate (f,(E-max (L~ f))))) ) by A12, MATRIX_0:32;

( 1 <= i & i <= len (GoB (Rotate (f,(E-max (L~ f))))) ) by A12, MATRIX_0:32;

then (f /. (((E-max (L~ f)) .. f) + 1)) `1 = ((GoB (Rotate (f,(E-max (L~ f))))) * (i,1)) `1 by A15, A16, GOBOARD5:2

.= (f /. ((E-max (L~ f)) .. f)) `1 by A14, A18, A17, GOBOARD5:2

.= E-bound (L~ f) by A9, EUCLID:52 ;

hence (Rotate (f,(E-max (L~ f)))) /. 2 in E-most (L~ f) by A10, A7, A8, SPRECT_2:13; :: thesis: verum

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:25, GOBOARD5:def 5;

then consider i2, j2 being 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 9;

A23: j2 <= width (GoB (Rotate (f,(E-max (L~ f))))) by A21, MATRIX_0:32;

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_0:32;

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:235;

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:235;

(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:50;

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:47;

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:47;

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:21;

Int (left_cell ((Rotate (f,(E-max (L~ f)))),1)) <> {} by A32, GOBOARD9:15;

then consider p being object 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:124;

A36: 1 <= j2 by A21, MATRIX_0:32;

A37: i_n_e (Rotate (f,(E-max (L~ f)))) <= width (GoB (Rotate (f,(E-max (L~ f))))) by A24, MATRIX_0:32;

rng (Rotate (f,(E-max (L~ f)))) = rng f by FINSEQ_6:90, SPRECT_2:46;

then 1 in dom (Rotate (f,(E-max (L~ f)))) by FINSEQ_3:31, SPRECT_2:46;

then |.(i2 - i2).| + |.((i_n_e (Rotate (f,(E-max (L~ f))))) - j2).| = 1 by A24, A28, A20, A21, A22, A31, GOBOARD1:def 9;

then A38: 0 + |.((i_n_e (Rotate (f,(E-max (L~ f))))) - j2).| = 1 by ABSVALUE:2;

A39: 1 <= len (GoB (Rotate (f,(E-max (L~ f))))) by A24, MATRIX_0:32;

((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:47;

then (i_n_e (Rotate (f,(E-max (L~ f))))) - j2 >= 0 by A39, A25, A31, A23, GOBOARD5:4, XREAL_1:48;

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:233;

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:27;

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:21;

(i_n_e (Rotate (f,(E-max (L~ f))))) - 1 < (i_n_e (Rotate (f,(E-max (L~ f))))) - 0 by XREAL_1:15;

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:23;

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 :: thesis: not east_halfline p meets L~ (Rotate (f,(E-max (L~ f))))

then A49:
east_halfline p c= UBD (L~ (Rotate (f,(E-max (L~ f)))))
by JORDAN2C:127;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 object 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 11;

then A48: a `1 >= t by A43, EUCLID:52;

((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:2;

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:52;

hence contradiction by A46, PSCOMP_1:24; :: thesis: verum

end;then (east_halfline p) /\ (L~ (Rotate (f,(E-max (L~ f))))) <> {} by XBOOLE_0:def 7;

then consider a being object 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 11;

then A48: a `1 >= t by A43, EUCLID:52;

((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:2;

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:52;

hence contradiction by A46, PSCOMP_1:24; :: thesis: verum

p in east_halfline p by TOPREAL1:38;

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:1, JORDAN1H:41;

hence f is clockwise_oriented by JORDAN1H:40; :: thesis: verum