:: Again on the Order on a Special Polygon
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received October 16, 2000
:: Copyright (c) 2000-2011 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
proof end;

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 & q in rng f & p .. f <= q .. f holds
q .. (f :- p) = ((q .. f) - (p .. f)) + 1
proof end;

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 & q in rng f & p .. f <= q .. f holds
p .. (f -: q) = p .. f
proof end;

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 & q in rng f & p .. f <= q .. f holds
q .. (Rotate (f,p)) = ((q .. f) - (p .. f)) + 1
proof end;

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 & p2 in rng f & p3 in rng f & p1 .. f <= p2 .. f & p2 .. f < p3 .. f holds
p2 .. (Rotate (f,p1)) < p3 .. (Rotate (f,p1))
proof end;

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 & p2 in rng f & p3 in rng f & p1 .. f < p2 .. f & p2 .. f <= p3 .. f holds
p2 .. (Rotate (f,p1)) <= p3 .. (Rotate (f,p1))
proof end;

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 & len g > 1 holds
p .. g < len g
proof end;

begin

theorem :: SPRECT_5:8
canceled;

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

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

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

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 & p2 in rng f & p3 in rng f & p1 .. f < p2 .. f & p2 .. f < p3 .. f holds
p3 .. (Rotate (f,p2)) < p1 .. (Rotate (f,p2))
proof end;

theorem Th12: :: 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 & p2 in rng f & p3 in rng f & p1 .. f < p2 .. f & p2 .. f < p3 .. f holds
p1 .. (Rotate (f,p3)) < p2 .. (Rotate (f,p3))
proof end;

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

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

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

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

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

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

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

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

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

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

theorem Th22: :: SPRECT_5:22
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
proof end;

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

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

theorem Th25: :: SPRECT_5:25
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
proof end;

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

theorem Th27: :: SPRECT_5:27
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
proof end;

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

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

theorem Th30: :: SPRECT_5:30
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
proof end;

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

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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

theorem Th33: :: SPRECT_5:33
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
proof end;

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

theorem Th35: :: SPRECT_5:35
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
proof end;

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

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

theorem Th38: :: SPRECT_5:38
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
proof end;

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

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

theorem Th41: :: SPRECT_5:41
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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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
proof end;

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

theorem Th43: :: SPRECT_5:43
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
proof end;

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

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

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

theorem :: SPRECT_5:47
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
proof end;

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

theorem :: SPRECT_5:49
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
proof end;

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

theorem :: SPRECT_5:51
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
proof end;

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

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

theorem :: SPRECT_5:54
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
proof end;

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

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
proof end;

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
proof end;

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
proof end;

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
proof end;

theorem :: SPRECT_5:56
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
proof end;

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

theorem :: SPRECT_5:58
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
proof end;

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

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

theorem :: SPRECT_5:61
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
proof end;

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

theorem :: SPRECT_5:63
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
proof end;

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

theorem :: SPRECT_5:65
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
proof end;

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

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

theorem :: SPRECT_5:68
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
proof end;

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

theorem :: SPRECT_5:70
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
proof end;

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

theorem :: SPRECT_5:72
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
proof end;

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