set j = 1;

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

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

A5: i2 <= len (GoB (Rotate (f,(S-max (L~ f))))) by A3, MATRIX_0:32;

set i = i_e_s (Rotate (f,(S-max (L~ f))));

A6: S-max (L~ f) in rng f by SPRECT_2:42;

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

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 )

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

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

.= (S-min (L~ f)) `2 by EUCLID:52 ;

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

then A28: j2 = 1 by A24, A3, JORDAN1G:6;

A29: 1 <= width (GoB (Rotate (f,(S-max (L~ f))))) by A24, MATRIX_0:32;

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

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

then |.(1 - 1).| + |.((i_e_s (Rotate (f,(S-max (L~ f))))) - i2).| = 1 by A1, A24, A27, A2, A3, A4, A28, GOBOARD1:def 9;

then A30: 0 + |.((i_e_s (Rotate (f,(S-max (L~ f))))) - i2).| = 1 by ABSVALUE:2;

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

then (i_e_s (Rotate (f,(S-max (L~ f))))) - i2 >= 0 by A25, A29, A28, A5, GOBOARD5:3, XREAL_1:48;

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

then A33: 1 <= (i_e_s (Rotate (f,(S-max (L~ f))))) -' 1 by A3, MATRIX_0:32;

A34: i_e_s (Rotate (f,(S-max (L~ f)))) <= len (GoB (Rotate (f,(S-max (L~ f))))) by A24, MATRIX_0:32;

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

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

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

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:25, XREAL_1:233;

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

(i_e_s (Rotate (f,(S-max (L~ f))))) - 1 < i_e_s (Rotate (f,(S-max (L~ f)))) by XREAL_1:146;

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

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

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;

p in south_halfline p by TOPREAL1:38;

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

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

A5: i2 <= len (GoB (Rotate (f,(S-max (L~ f))))) by A3, MATRIX_0:32;

set i = i_e_s (Rotate (f,(S-max (L~ f))));

A6: S-max (L~ f) in rng f by SPRECT_2:42;

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

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

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

(S-max (L~ f)) .. f < len f by SPRECT_5:14;

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

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

then A11: f /. (((S-max (L~ f)) .. f) + 1) in rng f by A10, FUNCT_1:3;

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

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

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

A20: ( 1 <= i + 1 & i + 1 <= len (GoB (Rotate (f,(S-max (L~ f))))) ) by A16, MATRIX_0:32;

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

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

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

then (f /. (((S-max (L~ f)) .. f) + 1)) `2 = ((GoB (Rotate (f,(S-max (L~ f))))) * (1,j)) `2 by A19, A21, GOBOARD5:1

.= (f /. ((S-max (L~ f)) .. f)) `2 by A18, A20, A22, GOBOARD5:1

.= S-bound (L~ f) by A13, EUCLID:52 ;

hence (Rotate (f,(S-max (L~ f)))) /. 2 in S-most (L~ f) by A14, A11, A12, SPRECT_2:11; :: thesis: verum

end;(S-max (L~ f)) .. f < len f by SPRECT_5:14;

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

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

then A11: f /. (((S-max (L~ f)) .. f) + 1) in rng f by A10, FUNCT_1:3;

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

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

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

A20: ( 1 <= i + 1 & i + 1 <= len (GoB (Rotate (f,(S-max (L~ f))))) ) by A16, MATRIX_0:32;

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

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

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

then (f /. (((S-max (L~ f)) .. f) + 1)) `2 = ((GoB (Rotate (f,(S-max (L~ f))))) * (1,j)) `2 by A19, A21, GOBOARD5:1

.= (f /. ((S-max (L~ f)) .. f)) `2 by A18, A20, A22, GOBOARD5:1

.= S-bound (L~ f) by A13, EUCLID:52 ;

hence (Rotate (f,(S-max (L~ f)))) /. 2 in S-most (L~ f) by A14, A11, A12, SPRECT_2:11; :: thesis: verum

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

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

.= (S-min (L~ f)) `2 by EUCLID:52 ;

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

then A28: j2 = 1 by A24, A3, JORDAN1G:6;

A29: 1 <= width (GoB (Rotate (f,(S-max (L~ f))))) by A24, MATRIX_0:32;

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

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

then |.(1 - 1).| + |.((i_e_s (Rotate (f,(S-max (L~ f))))) - i2).| = 1 by A1, A24, A27, A2, A3, A4, A28, GOBOARD1:def 9;

then A30: 0 + |.((i_e_s (Rotate (f,(S-max (L~ f))))) - i2).| = 1 by ABSVALUE:2;

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

then (i_e_s (Rotate (f,(S-max (L~ f))))) - i2 >= 0 by A25, A29, A28, A5, GOBOARD5:3, XREAL_1:48;

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

then A33: 1 <= (i_e_s (Rotate (f,(S-max (L~ f))))) -' 1 by A3, MATRIX_0:32;

A34: i_e_s (Rotate (f,(S-max (L~ f)))) <= len (GoB (Rotate (f,(S-max (L~ f))))) by A24, MATRIX_0:32;

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

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

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

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:25, XREAL_1:233;

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

(i_e_s (Rotate (f,(S-max (L~ f))))) - 1 < i_e_s (Rotate (f,(S-max (L~ f)))) by XREAL_1:146;

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

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

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

then A47:
south_halfline p c= UBD (L~ (Rotate (f,(S-max (L~ f)))))
by JORDAN2C:128;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 object 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 12;

then a `2 <= s by A41, EUCLID:52;

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

then a `2 < S-bound (L~ (Rotate (f,(S-max (L~ f))))) by A26, A7, A27, A46, EUCLID:52;

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

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

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

then a `2 <= s by A41, EUCLID:52;

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

then a `2 < S-bound (L~ (Rotate (f,(S-max (L~ f))))) by A26, A7, A27, A46, EUCLID:52;

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

p in south_halfline p by TOPREAL1:38;

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

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