let f be constant standard special_circular_sequence; ( 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) )
( (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: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
;
(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;
verum
end;
assume A19:
(Rotate (f,(E-max (L~ f)))) /. 2 in E-most (L~ f)
; 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;
now not east_halfline p meets L~ (Rotate (f,(E-max (L~ f))))assume
east_halfline p meets L~ (Rotate (f,(E-max (L~ f))))
;
contradictionthen
(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;
verum end;
then A49:
east_halfline p c= UBD (L~ (Rotate (f,(E-max (L~ f)))))
by JORDAN2C:127;
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; verum