:: Again on the Order on a Special Polygon
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received October 16, 2000
:: Copyright (c) 2000-2012 Association of Mizar Users


begin

theorem Th1: :: SPRECT_5:1
for D being non empty set
for f being FinSequence of D
for q, p being Element of D st q in rng (f | (p .. f)) holds
q .. f <= p .. f
proofend;

theorem Th2: :: SPRECT_5:2
for D being non empty set
for f being FinSequence of D
for p, q being Element of D st p in rng f &amp; q in rng f &amp; p .. f <= q .. f holds
q .. (f :- p) = ((q .. f) - (p .. f)) + 1
proofend;

theorem Th3: :: SPRECT_5:3
for D being non empty set
for f being FinSequence of D
for p, q being Element of D st p in rng f &amp; q in rng f &amp; p .. f <= q .. f holds
p .. (f -: q) = p .. f
proofend;

theorem Th4: :: SPRECT_5:4
for D being non empty set
for f being FinSequence of D
for p, q being Element of D st p in rng f &amp; q in rng f &amp; p .. f <= q .. f holds
q .. (Rotate (f,p)) = ((q .. f) - (p .. f)) + 1
proofend;

theorem Th5: :: SPRECT_5:5
for D being non empty set
for f being FinSequence of D
for p1, p2, p3 being Element of D st p1 in rng f &amp; p2 in rng f &amp; p3 in rng f &amp; p1 .. f <= p2 .. f &amp; p2 .. f < p3 .. f holds
p2 .. (Rotate (f,p1)) < p3 .. (Rotate (f,p1))
proofend;

theorem :: SPRECT_5:6
for D being non empty set
for f being FinSequence of D
for p1, p2, p3 being Element of D st p1 in rng f &amp; p2 in rng f &amp; p3 in rng f &amp; p1 .. f < p2 .. f &amp; p2 .. f <= p3 .. f holds
p2 .. (Rotate (f,p1)) <= p3 .. (Rotate (f,p1))
proofend;

theorem Th7: :: SPRECT_5:7
for D being non empty set
for g being circular FinSequence of D
for p being Element of D st p in rng g &amp; len g > 1 holds
p .. g < len g
proofend;

begin

registration
let f be non constant standard special_circular_sequence;
clusterf /^ 1 ->  one-to-one ;
coherence
 f /^ 1 is one-to-one
proofend;
end;

theorem Th8: :: SPRECT_5:8
for f being non constant standard special_circular_sequence
for q being Point of (TOP-REAL 2) st 1 < q .. f &amp; q in rng f holds
(f /. 1) .. (Rotate (f,q)) = ((len f) + 1) - (q .. f)
proofend;

theorem Th9: :: SPRECT_5:9
for f being non constant standard special_circular_sequence
for p, q being Point of (TOP-REAL 2) st p in rng f &amp; q in rng f &amp; p .. f < q .. f holds
p .. (Rotate (f,q)) = ((len f) + (p .. f)) - (q .. f)
proofend;

theorem Th10: :: SPRECT_5:10
for f being non constant standard special_circular_sequence
for p1, p2, p3 being Point of (TOP-REAL 2) st p1 in rng f &amp; p2 in rng f &amp; p3 in rng f &amp; p1 .. f < p2 .. f &amp; p2 .. f < p3 .. f holds
p3 .. (Rotate (f,p2)) < p1 .. (Rotate (f,p2))
proofend;

theorem Th11: :: SPRECT_5:11
for f being non constant standard special_circular_sequence
for p1, p2, p3 being Point of (TOP-REAL 2) st p1 in rng f &amp; p2 in rng f &amp; p3 in rng f &amp; p1 .. f < p2 .. f &amp; p2 .. f < p3 .. f holds
p1 .. (Rotate (f,p3)) < p2 .. (Rotate (f,p3))
proofend;

theorem :: SPRECT_5:12
for f being non constant standard special_circular_sequence
for p1, p2, p3 being Point of (TOP-REAL 2) st p1 in rng f &amp; p2 in rng f &amp; p3 in rng f &amp; p1 .. f <= p2 .. f &amp; p2 .. f < p3 .. f holds
p1 .. (Rotate (f,p3)) <= p2 .. (Rotate (f,p3))
proofend;

theorem :: SPRECT_5:13
for f being non constant standard special_circular_sequence holds (S-min (L~ f)) .. f < len f
proofend;

theorem :: SPRECT_5:14
for f being non constant standard special_circular_sequence holds (S-max (L~ f)) .. f < len f
proofend;

theorem :: SPRECT_5:15
for f being non constant standard special_circular_sequence holds (E-min (L~ f)) .. f < len f
proofend;

theorem :: SPRECT_5:16
for f being non constant standard special_circular_sequence holds (E-max (L~ f)) .. f < len f
proofend;

theorem :: SPRECT_5:17
for f being non constant standard special_circular_sequence holds (N-min (L~ f)) .. f < len f
proofend;

theorem :: SPRECT_5:18
for f being non constant standard special_circular_sequence holds (N-max (L~ f)) .. f < len f
proofend;

theorem :: SPRECT_5:19
for f being non constant standard special_circular_sequence holds (W-max (L~ f)) .. f < len f
proofend;

theorem :: SPRECT_5:20
for f being non constant standard special_circular_sequence holds (W-min (L~ f)) .. f < len f
proofend;

begin

Lm1:  for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) holds
(E-max (L~ z)) .. z < (S-max (L~ z)) .. z
proofend;

Lm2:  for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) holds
(E-max (L~ z)) .. z < (S-min (L~ z)) .. z
proofend;

Lm3:  for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) holds
(E-max (L~ z)) .. z < (W-min (L~ z)) .. z
proofend;

Lm4:  for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) holds
(E-min (L~ z)) .. z < (S-min (L~ z)) .. z
proofend;

Lm5:  for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) holds
(E-min (L~ z)) .. z < (W-min (L~ z)) .. z
proofend;

Lm6:  for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) holds
(S-max (L~ z)) .. z < (W-min (L~ z)) .. z
proofend;

Lm7:  for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) holds
(N-max (L~ z)) .. z < (W-min (L~ z)) .. z
proofend;

Lm8:  for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) holds
(N-min (L~ z)) .. z < (W-min (L~ z)) .. z
proofend;

Lm9:  for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) holds
(N-max (L~ z)) .. z < (S-max (L~ z)) .. z
proofend;

Lm10:  for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) holds
(N-max (L~ z)) .. z < (S-min (L~ z)) .. z
proofend;

theorem Th21: :: SPRECT_5:21
for f being non constant standard special_circular_sequence st f /. 1 = W-min (L~ f) holds
(W-min (L~ f)) .. f < (W-max (L~ f)) .. f
proofend;

theorem :: SPRECT_5:22
for f being non constant standard special_circular_sequence st f /. 1 = W-min (L~ f) holds
(W-max (L~ f)) .. f > 1
proofend;

theorem Th23: :: SPRECT_5:23
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = W-min (L~ z) &amp; W-max (L~ z) <> N-min (L~ z) holds
(W-max (L~ z)) .. z < (N-min (L~ z)) .. z
proofend;

theorem Th24: :: SPRECT_5:24
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = W-min (L~ z) holds
(N-min (L~ z)) .. z < (N-max (L~ z)) .. z
proofend;

theorem Th25: :: SPRECT_5:25
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = W-min (L~ z) &amp; N-max (L~ z) <> E-max (L~ z) holds
(N-max (L~ z)) .. z < (E-max (L~ z)) .. z
proofend;

theorem Th26: :: SPRECT_5:26
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = W-min (L~ z) holds
(E-max (L~ z)) .. z < (E-min (L~ z)) .. z
proofend;

theorem Th27: :: SPRECT_5:27
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = W-min (L~ z) &amp; E-min (L~ z) <> S-max (L~ z) holds
(E-min (L~ z)) .. z < (S-max (L~ z)) .. z
proofend;

theorem :: SPRECT_5:28
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = W-min (L~ z) &amp; S-min (L~ z) <> W-min (L~ z) holds
(S-max (L~ z)) .. z < (S-min (L~ z)) .. z
proofend;

theorem Th29: :: SPRECT_5:29
for f being non constant standard special_circular_sequence st f /. 1 = S-max (L~ f) holds
(S-max (L~ f)) .. f < (S-min (L~ f)) .. f
proofend;

theorem :: SPRECT_5:30
for f being non constant standard special_circular_sequence st f /. 1 = S-max (L~ f) holds
(S-min (L~ f)) .. f > 1
proofend;

Lm11:  for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = W-min (L~ z) holds
(E-max (L~ z)) .. z < (S-max (L~ z)) .. z
proofend;

Lm12:  for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = W-min (L~ z) holds
(N-min (L~ z)) .. z < (E-max (L~ z)) .. z
proofend;

Lm13:  for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = W-min (L~ z) holds
(N-min (L~ z)) .. z < (S-max (L~ z)) .. z
proofend;

Lm14:  for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = W-min (L~ z) holds
(N-max (L~ z)) .. z < (S-max (L~ z)) .. z
proofend;

Lm15:  for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = W-min (L~ z) holds
(W-max (L~ z)) .. z < (S-max (L~ z)) .. z
proofend;

Lm16:  for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = W-min (L~ z) holds
(N-max (L~ z)) .. z < (E-min (L~ z)) .. z
proofend;

Lm17:  for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = W-min (L~ z) holds
(N-min (L~ z)) .. z < (E-max (L~ z)) .. z
proofend;

Lm18:  for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = W-min (L~ z) holds
(W-max (L~ z)) .. z < (E-max (L~ z)) .. z
proofend;

Lm19:  for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = W-min (L~ z) holds
(W-max (L~ z)) .. z < (E-min (L~ z)) .. z
proofend;

theorem Th31: :: SPRECT_5:31
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = S-max (L~ z) &amp; S-min (L~ z) <> W-min (L~ z) holds
(S-min (L~ z)) .. z < (W-min (L~ z)) .. z
proofend;

theorem Th32: :: SPRECT_5:32
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = S-max (L~ z) holds
(W-min (L~ z)) .. z < (W-max (L~ z)) .. z
proofend;

theorem Th33: :: SPRECT_5:33
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = S-max (L~ z) &amp; W-max (L~ z) <> N-min (L~ z) holds
(W-max (L~ z)) .. z < (N-min (L~ z)) .. z
proofend;

theorem Th34: :: SPRECT_5:34
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = S-max (L~ z) holds
(N-min (L~ z)) .. z < (N-max (L~ z)) .. z
proofend;

theorem Th35: :: SPRECT_5:35
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = S-max (L~ z) &amp; N-max (L~ z) <> E-max (L~ z) holds
(N-max (L~ z)) .. z < (E-max (L~ z)) .. z
proofend;

theorem :: SPRECT_5:36
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = S-max (L~ z) &amp; E-min (L~ z) <> S-max (L~ z) holds
(E-max (L~ z)) .. z < (E-min (L~ z)) .. z
proofend;

theorem Th37: :: SPRECT_5:37
for f being non constant standard special_circular_sequence st f /. 1 = E-max (L~ f) holds
(E-max (L~ f)) .. f < (E-min (L~ f)) .. f
proofend;

theorem :: SPRECT_5:38
for f being non constant standard special_circular_sequence st f /. 1 = E-max (L~ f) holds
(E-min (L~ f)) .. f > 1
proofend;

theorem Th39: :: SPRECT_5:39
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = E-max (L~ z) &amp; S-max (L~ z) <> E-min (L~ z) holds
(E-min (L~ z)) .. z < (S-max (L~ z)) .. z
proofend;

theorem Th40: :: SPRECT_5:40
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = E-max (L~ z) holds
(S-max (L~ z)) .. z < (S-min (L~ z)) .. z
proofend;

Lm20:  for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = S-max (L~ z) holds
(N-min (L~ z)) .. z < (E-max (L~ z)) .. z
proofend;

Lm21:  for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = S-max (L~ z) holds
(W-max (L~ z)) .. z < (E-max (L~ z)) .. z
proofend;

Lm22:  for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = S-max (L~ z) holds
(W-min (L~ z)) .. z < (E-max (L~ z)) .. z
proofend;

Lm23:  for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = S-max (L~ z) holds
(W-max (L~ z)) .. z < (N-max (L~ z)) .. z
proofend;

Lm24:  for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = S-max (L~ z) holds
(W-min (L~ z)) .. z < (N-min (L~ z)) .. z
proofend;

Lm25:  for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = S-max (L~ z) holds
(S-min (L~ z)) .. z < (N-min (L~ z)) .. z
proofend;

Lm26:  for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = S-max (L~ z) holds
(S-min (L~ z)) .. z < (N-max (L~ z)) .. z
proofend;

theorem Th41: :: SPRECT_5:41
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = E-max (L~ z) &amp; S-min (L~ z) <> W-min (L~ z) holds
(S-min (L~ z)) .. z < (W-min (L~ z)) .. z
proofend;

theorem Th42: :: SPRECT_5:42
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = E-max (L~ z) holds
(W-min (L~ z)) .. z < (W-max (L~ z)) .. z
proofend;

theorem Th43: :: SPRECT_5:43
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = E-max (L~ z) &amp; W-max (L~ z) <> N-min (L~ z) holds
(W-max (L~ z)) .. z < (N-min (L~ z)) .. z
proofend;

theorem :: SPRECT_5:44
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = E-max (L~ z) &amp; N-max (L~ z) <> E-max (L~ z) holds
(N-min (L~ z)) .. z < (N-max (L~ z)) .. z
proofend;

theorem :: SPRECT_5:45
for f being non constant standard special_circular_sequence st f /. 1 = N-max (L~ f) &amp; N-max (L~ f) <> E-max (L~ f) holds
(N-max (L~ f)) .. f < (E-max (L~ f)) .. f
proofend;

theorem :: SPRECT_5:46
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-max (L~ z) holds
(E-max (L~ z)) .. z < (E-min (L~ z)) .. z
proofend;

theorem :: SPRECT_5:47
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-max (L~ z) &amp; E-min (L~ z) <> S-max (L~ z) holds
(E-min (L~ z)) .. z < (S-max (L~ z)) .. z
proofend;

theorem :: SPRECT_5:48
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-max (L~ z) holds
(S-max (L~ z)) .. z < (S-min (L~ z)) .. z
proofend;

theorem :: SPRECT_5:49
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-max (L~ z) &amp; S-min (L~ z) <> W-min (L~ z) holds
(S-min (L~ z)) .. z < (W-min (L~ z)) .. z
proofend;

theorem :: SPRECT_5:50
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-max (L~ z) holds
(W-min (L~ z)) .. z < (W-max (L~ z)) .. z
proofend;

theorem :: SPRECT_5:51
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = N-max (L~ z) &amp; N-min (L~ z) <> W-max (L~ z) holds
(W-max (L~ z)) .. z < (N-min (L~ z)) .. z
proofend;

theorem :: SPRECT_5:52
for f being non constant standard special_circular_sequence st f /. 1 = E-min (L~ f) &amp; E-min (L~ f) <> S-max (L~ f) holds
(E-min (L~ f)) .. f < (S-max (L~ f)) .. f
proofend;

theorem :: SPRECT_5:53
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = E-min (L~ z) holds
(S-max (L~ z)) .. z < (S-min (L~ z)) .. z
proofend;

theorem :: SPRECT_5:54
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = E-min (L~ z) &amp; S-min (L~ z) <> W-min (L~ z) holds
(S-min (L~ z)) .. z < (W-min (L~ z)) .. z
proofend;

Lm27:  for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = E-max (L~ z) holds
(S-max (L~ z)) .. z < (W-min (L~ z)) .. z
proofend;

Lm28:  for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = E-max (L~ z) holds
(E-min (L~ z)) .. z < (W-min (L~ z)) .. z
proofend;

Lm29:  for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = E-max (L~ z) holds
(E-min (L~ z)) .. z < (W-max (L~ z)) .. z
proofend;

Lm30:  for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = E-max (L~ z) holds
(S-min (L~ z)) .. z < (W-max (L~ z)) .. z
proofend;

theorem :: SPRECT_5:55
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = E-min (L~ z) holds
(W-min (L~ z)) .. z < (W-max (L~ z)) .. z
proofend;

theorem :: SPRECT_5:56
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = E-min (L~ z) &amp; W-max (L~ z) <> N-min (L~ z) holds
(W-max (L~ z)) .. z < (N-min (L~ z)) .. z
proofend;

theorem :: SPRECT_5:57
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = E-min (L~ z) holds
(N-min (L~ z)) .. z < (N-max (L~ z)) .. z
proofend;

theorem :: SPRECT_5:58
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = E-min (L~ z) &amp; E-max (L~ z) <> N-max (L~ z) holds
(N-max (L~ z)) .. z < (E-max (L~ z)) .. z
proofend;

theorem :: SPRECT_5:59
for f being non constant standard special_circular_sequence st f /. 1 = S-min (L~ f) &amp; S-min (L~ f) <> W-min (L~ f) holds
(S-min (L~ f)) .. f < (W-min (L~ f)) .. f
proofend;

theorem :: SPRECT_5:60
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = S-min (L~ z) holds
(W-min (L~ z)) .. z < (W-max (L~ z)) .. z
proofend;

theorem :: SPRECT_5:61
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = S-min (L~ z) &amp; W-max (L~ z) <> N-min (L~ z) holds
(W-max (L~ z)) .. z < (N-min (L~ z)) .. z
proofend;

theorem :: SPRECT_5:62
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = S-min (L~ z) holds
(N-min (L~ z)) .. z < (N-max (L~ z)) .. z
proofend;

theorem :: SPRECT_5:63
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = S-min (L~ z) &amp; N-max (L~ z) <> E-max (L~ z) holds
(N-max (L~ z)) .. z < (E-max (L~ z)) .. z
proofend;

theorem :: SPRECT_5:64
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = S-min (L~ z) holds
(E-max (L~ z)) .. z < (E-min (L~ z)) .. z
proofend;

theorem :: SPRECT_5:65
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = S-min (L~ z) &amp; S-max (L~ z) <> E-min (L~ z) holds
(E-min (L~ z)) .. z < (S-max (L~ z)) .. z
proofend;

theorem :: SPRECT_5:66
for f being non constant standard special_circular_sequence st f /. 1 = W-max (L~ f) &amp; W-max (L~ f) <> N-min (L~ f) holds
(W-max (L~ f)) .. f < (N-min (L~ f)) .. f
proofend;

theorem :: SPRECT_5:67
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = W-max (L~ z) holds
(N-min (L~ z)) .. z < (N-max (L~ z)) .. z
proofend;

theorem :: SPRECT_5:68
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = W-max (L~ z) &amp; N-max (L~ z) <> E-max (L~ z) holds
(N-max (L~ z)) .. z < (E-max (L~ z)) .. z
proofend;

theorem :: SPRECT_5:69
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = W-max (L~ z) holds
(E-max (L~ z)) .. z < (E-min (L~ z)) .. z
proofend;

theorem :: SPRECT_5:70
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = W-max (L~ z) &amp; E-min (L~ z) <> S-max (L~ z) holds
(E-min (L~ z)) .. z < (S-max (L~ z)) .. z
proofend;

theorem :: SPRECT_5:71
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = W-max (L~ z) holds
(S-max (L~ z)) .. z < (S-min (L~ z)) .. z
proofend;

theorem :: SPRECT_5:72
for z being non constant standard clockwise_oriented special_circular_sequence st z /. 1 = W-max (L~ z) &amp; W-min (L~ z) <> S-min (L~ z) holds
(S-min (L~ z)) .. z < (W-min (L~ z)) .. z
proofend;