set i = 1;

let f be V22() 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: Rotate (f,(W-min (L~ f))) is_sequence_on GoB (Rotate (f,(W-min (L~ f)))) by GOBOARD5:def 5;

A2: 1 + 1 <= len (Rotate (f,(W-min (L~ f)))) by TOPREAL8:3;

then A3: Int (left_cell ((Rotate (f,(W-min (L~ f)))),1)) c= LeftComp (Rotate (f,(W-min (L~ f)))) by GOBOARD9:21;

set j = i_s_w (Rotate (f,(W-min (L~ f))));

A4: W-min (L~ f) in rng f by SPRECT_2:43;

then A5: (Rotate (f,(W-min (L~ f)))) /. 1 = W-min (L~ f) by FINSEQ_6:92;

A6: 2 <= len f by TOPREAL8:3;

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 )

then A22: ( 1 <= len (GoB (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_0:32;

len (Rotate (f,(W-min (L~ f)))) > 2 by TOPREAL8:3;

then A23: 1 + 1 in dom (Rotate (f,(W-min (L~ f)))) by FINSEQ_3:25;

then consider i2, j2 being Nat such that

A24: [i2,j2] in Indices (GoB (Rotate (f,(W-min (L~ f))))) and

A25: (Rotate (f,(W-min (L~ f)))) /. (1 + 1) = (GoB (Rotate (f,(W-min (L~ f))))) * (i2,j2) by A1, GOBOARD1:def 9;

A26: 1 <= j2 by A24, MATRIX_0:32;

A27: L~ (Rotate (f,(W-min (L~ f)))) = L~ f by REVROT_1:33;

then A28: (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 A5, JORDAN5D:def 1;

assume A29: (Rotate (f,(W-min (L~ f)))) /. 2 in W-most (L~ f) ; :: thesis: f is clockwise_oriented

then ((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 by A5, A28, A25, PSCOMP_1:31;

then A30: i2 = 1 by A21, A24, JORDAN1G:7;

rng (Rotate (f,(W-min (L~ f)))) = rng f by FINSEQ_6:90, SPRECT_2:43;

then 1 in dom (Rotate (f,(W-min (L~ f)))) by FINSEQ_3:31, SPRECT_2:43;

then |.(1 - 1).| + |.((i_s_w (Rotate (f,(W-min (L~ f))))) - j2).| = 1 by A1, A21, A28, A23, A24, A25, A30, GOBOARD1:def 9;

then 0 + |.((i_s_w (Rotate (f,(W-min (L~ f))))) - j2).| = 1 by ABSVALUE:2;

then A31: |.(j2 - (i_s_w (Rotate (f,(W-min (L~ f)))))).| = 1 by UNIFORM1:11;

((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 A5, A28, A29, A25, PSCOMP_1:31;

then j2 - (i_s_w (Rotate (f,(W-min (L~ f))))) >= 0 by A22, A30, A26, GOBOARD5:4, XREAL_1:48;

then A32: j2 - (i_s_w (Rotate (f,(W-min (L~ f))))) = 1 by A31, ABSVALUE:def 1;

then j2 = (i_s_w (Rotate (f,(W-min (L~ f))))) + 1 ;

then ( 1 -' 1 = 1 - 1 & 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 A2, A1, A21, A28, A24, A25, A30, GOBRD13:21, XREAL_1:233;

then A33: 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 A2, JORDAN1H:21;

Int (left_cell ((Rotate (f,(W-min (L~ f)))),1)) <> {} by A2, GOBOARD9:15;

then consider p being object such that

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

A35: ( LeftComp (Rotate (f,(W-min (L~ f)))) is_a_component_of (L~ (Rotate (f,(W-min (L~ f))))) ` & UBD (L~ (Rotate (f,(W-min (L~ f))))) is_a_component_of (L~ (Rotate (f,(W-min (L~ f))))) ` ) by GOBOARD9:def 1, JORDAN2C:124;

A36: 1 <= i_s_w (Rotate (f,(W-min (L~ f)))) by A21, MATRIX_0:32;

(i_s_w (Rotate (f,(W-min (L~ f))))) + 1 <= width (GoB (Rotate (f,(W-min (L~ f))))) by A24, A32, MATRIX_0:32;

then i_s_w (Rotate (f,(W-min (L~ f)))) < width (GoB (Rotate (f,(W-min (L~ f))))) by NAT_1:13;

then 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 A36, A33, GOBOARD6:20;

then consider t, s being Real such that

A37: p = |[t,s]| and

A38: t < ((GoB (Rotate (f,(W-min (L~ f))))) * (1,1)) `1 and

((GoB (Rotate (f,(W-min (L~ f))))) * (1,(i_s_w (Rotate (f,(W-min (L~ f))))))) `2 < s and

s < ((GoB (Rotate (f,(W-min (L~ f))))) * (1,((i_s_w (Rotate (f,(W-min (L~ f))))) + 1))) `2 by A34;

p in west_halfline p by TOPREAL1:38;

then LeftComp (Rotate (f,(W-min (L~ f)))) meets UBD (L~ (Rotate (f,(W-min (L~ f))))) by A3, A34, A43, XBOOLE_0:3;

then Rotate (f,(W-min (L~ f))) is clockwise_oriented by A35, GOBOARD9:1, JORDAN1H:41;

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

let f be V22() 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: Rotate (f,(W-min (L~ f))) is_sequence_on GoB (Rotate (f,(W-min (L~ f)))) by GOBOARD5:def 5;

A2: 1 + 1 <= len (Rotate (f,(W-min (L~ f)))) by TOPREAL8:3;

then A3: Int (left_cell ((Rotate (f,(W-min (L~ f)))),1)) c= LeftComp (Rotate (f,(W-min (L~ f)))) by GOBOARD9:21;

set j = i_s_w (Rotate (f,(W-min (L~ f))));

A4: W-min (L~ f) in rng f by SPRECT_2:43;

then A5: (Rotate (f,(W-min (L~ f)))) /. 1 = W-min (L~ f) by FINSEQ_6:92;

A6: 2 <= len f by TOPREAL8:3;

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

A21:
[1,(i_s_w (Rotate (f,(W-min (L~ f)))))] in Indices (GoB (Rotate (f,(W-min (L~ f)))))
by JORDAN5D:def 1;
set k = (W-min (L~ f)) .. f;

(W-min (L~ f)) .. f < len f by SPRECT_5:20;

then A7: ((W-min (L~ f)) .. f) + 1 <= len f by NAT_1:13;

1 <= ((W-min (L~ f)) .. f) + 1 by NAT_1:11;

then A8: ((W-min (L~ f)) .. f) + 1 in dom f by A7, FINSEQ_3:25;

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

then A9: f /. (((W-min (L~ f)) .. f) + 1) in rng f by A8, FUNCT_1:3;

A10: rng f c= L~ f by A6, SPPOL_2:18;

A11: f /. ((W-min (L~ f)) .. f) = W-min (L~ f) by A4, FINSEQ_5:38;

(W-min (L~ f)) .. f <= ((W-min (L~ f)) .. f) + 1 by NAT_1:13;

then A12: 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 A4, A7, FINSEQ_6:175

.= (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 ;

f is_sequence_on GoB f by GOBOARD5:def 5;

then A13: f is_sequence_on GoB (Rotate (f,(W-min (L~ f)))) by REVROT_1:28;

assume f is clockwise_oriented ; :: thesis: (Rotate (f,(W-min (L~ f)))) /. 2 in W-most (L~ f)

then consider i, j being Nat such that

A14: [i,j] in Indices (GoB (Rotate (f,(W-min (L~ f))))) and

A15: [i,(j + 1)] in Indices (GoB (Rotate (f,(W-min (L~ f))))) and

A16: f /. ((W-min (L~ f)) .. f) = (GoB (Rotate (f,(W-min (L~ f))))) * (i,j) and

A17: f /. (((W-min (L~ f)) .. f) + 1) = (GoB (Rotate (f,(W-min (L~ f))))) * (i,(j + 1)) by A4, A7, A11, A13, Th21, FINSEQ_4:21;

A18: ( 1 <= i & i <= len (GoB (Rotate (f,(W-min (L~ f))))) ) by A14, MATRIX_0:32;

A19: ( 1 <= j + 1 & j + 1 <= width (GoB (Rotate (f,(W-min (L~ f))))) ) by A15, MATRIX_0:32;

A20: ( 1 <= j & j <= width (GoB (Rotate (f,(W-min (L~ f))))) ) by A14, MATRIX_0:32;

( 1 <= i & i <= len (GoB (Rotate (f,(W-min (L~ f))))) ) by A14, MATRIX_0:32;

then (f /. (((W-min (L~ f)) .. f) + 1)) `1 = ((GoB (Rotate (f,(W-min (L~ f))))) * (i,1)) `1 by A17, A19, GOBOARD5:2

.= (f /. ((W-min (L~ f)) .. f)) `1 by A16, A18, A20, GOBOARD5:2

.= W-bound (L~ f) by A11, EUCLID:52 ;

hence (Rotate (f,(W-min (L~ f)))) /. 2 in W-most (L~ f) by A12, A9, A10, SPRECT_2:12; :: thesis: verum

end;(W-min (L~ f)) .. f < len f by SPRECT_5:20;

then A7: ((W-min (L~ f)) .. f) + 1 <= len f by NAT_1:13;

1 <= ((W-min (L~ f)) .. f) + 1 by NAT_1:11;

then A8: ((W-min (L~ f)) .. f) + 1 in dom f by A7, FINSEQ_3:25;

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

then A9: f /. (((W-min (L~ f)) .. f) + 1) in rng f by A8, FUNCT_1:3;

A10: rng f c= L~ f by A6, SPPOL_2:18;

A11: f /. ((W-min (L~ f)) .. f) = W-min (L~ f) by A4, FINSEQ_5:38;

(W-min (L~ f)) .. f <= ((W-min (L~ f)) .. f) + 1 by NAT_1:13;

then A12: 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 A4, A7, FINSEQ_6:175

.= (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 ;

f is_sequence_on GoB f by GOBOARD5:def 5;

then A13: f is_sequence_on GoB (Rotate (f,(W-min (L~ f)))) by REVROT_1:28;

assume f is clockwise_oriented ; :: thesis: (Rotate (f,(W-min (L~ f)))) /. 2 in W-most (L~ f)

then consider i, j being Nat such that

A14: [i,j] in Indices (GoB (Rotate (f,(W-min (L~ f))))) and

A15: [i,(j + 1)] in Indices (GoB (Rotate (f,(W-min (L~ f))))) and

A16: f /. ((W-min (L~ f)) .. f) = (GoB (Rotate (f,(W-min (L~ f))))) * (i,j) and

A17: f /. (((W-min (L~ f)) .. f) + 1) = (GoB (Rotate (f,(W-min (L~ f))))) * (i,(j + 1)) by A4, A7, A11, A13, Th21, FINSEQ_4:21;

A18: ( 1 <= i & i <= len (GoB (Rotate (f,(W-min (L~ f))))) ) by A14, MATRIX_0:32;

A19: ( 1 <= j + 1 & j + 1 <= width (GoB (Rotate (f,(W-min (L~ f))))) ) by A15, MATRIX_0:32;

A20: ( 1 <= j & j <= width (GoB (Rotate (f,(W-min (L~ f))))) ) by A14, MATRIX_0:32;

( 1 <= i & i <= len (GoB (Rotate (f,(W-min (L~ f))))) ) by A14, MATRIX_0:32;

then (f /. (((W-min (L~ f)) .. f) + 1)) `1 = ((GoB (Rotate (f,(W-min (L~ f))))) * (i,1)) `1 by A17, A19, GOBOARD5:2

.= (f /. ((W-min (L~ f)) .. f)) `1 by A16, A18, A20, GOBOARD5:2

.= W-bound (L~ f) by A11, EUCLID:52 ;

hence (Rotate (f,(W-min (L~ f)))) /. 2 in W-most (L~ f) by A12, A9, A10, SPRECT_2:12; :: thesis: verum

then A22: ( 1 <= len (GoB (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_0:32;

len (Rotate (f,(W-min (L~ f)))) > 2 by TOPREAL8:3;

then A23: 1 + 1 in dom (Rotate (f,(W-min (L~ f)))) by FINSEQ_3:25;

then consider i2, j2 being Nat such that

A24: [i2,j2] in Indices (GoB (Rotate (f,(W-min (L~ f))))) and

A25: (Rotate (f,(W-min (L~ f)))) /. (1 + 1) = (GoB (Rotate (f,(W-min (L~ f))))) * (i2,j2) by A1, GOBOARD1:def 9;

A26: 1 <= j2 by A24, MATRIX_0:32;

A27: L~ (Rotate (f,(W-min (L~ f)))) = L~ f by REVROT_1:33;

then A28: (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 A5, JORDAN5D:def 1;

assume A29: (Rotate (f,(W-min (L~ f)))) /. 2 in W-most (L~ f) ; :: thesis: f is clockwise_oriented

then ((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 by A5, A28, A25, PSCOMP_1:31;

then A30: i2 = 1 by A21, A24, JORDAN1G:7;

rng (Rotate (f,(W-min (L~ f)))) = rng f by FINSEQ_6:90, SPRECT_2:43;

then 1 in dom (Rotate (f,(W-min (L~ f)))) by FINSEQ_3:31, SPRECT_2:43;

then |.(1 - 1).| + |.((i_s_w (Rotate (f,(W-min (L~ f))))) - j2).| = 1 by A1, A21, A28, A23, A24, A25, A30, GOBOARD1:def 9;

then 0 + |.((i_s_w (Rotate (f,(W-min (L~ f))))) - j2).| = 1 by ABSVALUE:2;

then A31: |.(j2 - (i_s_w (Rotate (f,(W-min (L~ f)))))).| = 1 by UNIFORM1:11;

((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 A5, A28, A29, A25, PSCOMP_1:31;

then j2 - (i_s_w (Rotate (f,(W-min (L~ f))))) >= 0 by A22, A30, A26, GOBOARD5:4, XREAL_1:48;

then A32: j2 - (i_s_w (Rotate (f,(W-min (L~ f))))) = 1 by A31, ABSVALUE:def 1;

then j2 = (i_s_w (Rotate (f,(W-min (L~ f))))) + 1 ;

then ( 1 -' 1 = 1 - 1 & 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 A2, A1, A21, A28, A24, A25, A30, GOBRD13:21, XREAL_1:233;

then A33: 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 A2, JORDAN1H:21;

Int (left_cell ((Rotate (f,(W-min (L~ f)))),1)) <> {} by A2, GOBOARD9:15;

then consider p being object such that

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

A35: ( LeftComp (Rotate (f,(W-min (L~ f)))) is_a_component_of (L~ (Rotate (f,(W-min (L~ f))))) ` & UBD (L~ (Rotate (f,(W-min (L~ f))))) is_a_component_of (L~ (Rotate (f,(W-min (L~ f))))) ` ) by GOBOARD9:def 1, JORDAN2C:124;

A36: 1 <= i_s_w (Rotate (f,(W-min (L~ f)))) by A21, MATRIX_0:32;

(i_s_w (Rotate (f,(W-min (L~ f))))) + 1 <= width (GoB (Rotate (f,(W-min (L~ f))))) by A24, A32, MATRIX_0:32;

then i_s_w (Rotate (f,(W-min (L~ f)))) < width (GoB (Rotate (f,(W-min (L~ f))))) by NAT_1:13;

then 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 A36, A33, GOBOARD6:20;

then consider t, s being Real such that

A37: p = |[t,s]| and

A38: t < ((GoB (Rotate (f,(W-min (L~ f))))) * (1,1)) `1 and

((GoB (Rotate (f,(W-min (L~ f))))) * (1,(i_s_w (Rotate (f,(W-min (L~ f))))))) `2 < s and

s < ((GoB (Rotate (f,(W-min (L~ f))))) * (1,((i_s_w (Rotate (f,(W-min (L~ f))))) + 1))) `2 by A34;

now :: thesis: not west_halfline p meets L~ (Rotate (f,(W-min (L~ f))))

then A43:
west_halfline p c= UBD (L~ (Rotate (f,(W-min (L~ f)))))
by JORDAN2C:126;A39:
((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 A36, A22, GOBOARD5:2;

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 object such that

A40: a in (west_halfline p) /\ (L~ (Rotate (f,(W-min (L~ f))))) by XBOOLE_0:def 1;

A41: a in L~ (Rotate (f,(W-min (L~ f)))) by A40, XBOOLE_0:def 4;

A42: a in west_halfline p by A40, XBOOLE_0:def 4;

reconsider a = a as Point of (TOP-REAL 2) by A40;

a `1 <= p `1 by A42, TOPREAL1:def 13;

then a `1 <= t by A37, EUCLID:52;

then a `1 < ((GoB (Rotate (f,(W-min (L~ f))))) * (1,(i_s_w (Rotate (f,(W-min (L~ f))))))) `1 by A38, A39, XXREAL_0:2;

then a `1 < W-bound (L~ (Rotate (f,(W-min (L~ f))))) by A27, A5, A28, EUCLID:52;

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

end;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 object such that

A40: a in (west_halfline p) /\ (L~ (Rotate (f,(W-min (L~ f))))) by XBOOLE_0:def 1;

A41: a in L~ (Rotate (f,(W-min (L~ f)))) by A40, XBOOLE_0:def 4;

A42: a in west_halfline p by A40, XBOOLE_0:def 4;

reconsider a = a as Point of (TOP-REAL 2) by A40;

a `1 <= p `1 by A42, TOPREAL1:def 13;

then a `1 <= t by A37, EUCLID:52;

then a `1 < ((GoB (Rotate (f,(W-min (L~ f))))) * (1,(i_s_w (Rotate (f,(W-min (L~ f))))))) `1 by A38, A39, XXREAL_0:2;

then a `1 < W-bound (L~ (Rotate (f,(W-min (L~ f))))) by A27, A5, A28, EUCLID:52;

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

p in west_halfline p by TOPREAL1:38;

then LeftComp (Rotate (f,(W-min (L~ f)))) meets UBD (L~ (Rotate (f,(W-min (L~ f))))) by A3, A34, A43, XBOOLE_0:3;

then Rotate (f,(W-min (L~ f))) is clockwise_oriented by A35, GOBOARD9:1, JORDAN1H:41;

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