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