:: SPRECT_5 semantic presentation

theorem Th1: :: SPRECT_5:1

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃, b₄ being Element of b₁ st b₃ in rng (b₂ | (b₄ .. b₂)) holds
b₃ .. b₂ <= b₄ .. b₂

proof end;

theorem Th2: :: SPRECT_5:2

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃, b₄ being Element of b₁ st b₃ in rng b₂ & b₄ in rng b₂ & b₃ .. b₂ <= b₄ .. b₂ holds
b₄ .. (b₂ :- b₃) = ((b₄ .. b₂) - (b₃ .. b₂)) + 1

proof end;

theorem Th3: :: SPRECT_5:3

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃, b₄ being Element of b₁ st b₃ in rng b₂ & b₄ in rng b₂ & b₃ .. b₂ <= b₄ .. b₂ holds
b₃ .. (b₂ -: b₄) = b₃ .. b₂

proof end;

theorem Th4: :: SPRECT_5:4

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃, b₄ being Element of b₁ st b₃ in rng b₂ & b₄ in rng b₂ & b₃ .. b₂ <= b₄ .. b₂ holds
b₄ .. (Rotate b₂,b₃) = ((b₄ .. b₂) - (b₃ .. b₂)) + 1

proof end;

theorem Th5: :: SPRECT_5:5

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃, b₄, b₅ being Element of b₁ st b₃ in rng b₂ & b₄ in rng b₂ & b₅ in rng b₂ & b₃ .. b₂ <= b₄ .. b₂ & b₄ .. b₂ < b₅ .. b₂ holds
b₄ .. (Rotate b₂,b₃) < b₅ .. (Rotate b₂,b₃)

proof end;

theorem Th6: :: SPRECT_5:6

for b₁ being non empty set
for b₂ being FinSequence of b₁
for b₃, b₄, b₅ being Element of b₁ st b₃ in rng b₂ & b₄ in rng b₂ & b₅ in rng b₂ & b₃ .. b₂ < b₄ .. b₂ & b₄ .. b₂ <= b₅ .. b₂ holds
b₄ .. (Rotate b₂,b₃) <= b₅ .. (Rotate b₂,b₃)

proof end;

theorem Th7: :: SPRECT_5:7

for b₁ being non empty set
for b₂ being circular FinSequence of b₁
for b₃ being Element of b₁ st b₃ in rng b₂ & len b₂ > 1 holds
b₃ .. b₂ < len b₂

proof end;

theorem Th8: :: SPRECT_5:8

for b₁ being standard non constant special_circular_sequence holds b₁ /^ 1 is one-to-one

proof end;

theorem Th9: :: SPRECT_5:9

for b₁ being standard non constant special_circular_sequence
for b₂ being Point of (TOP-REAL 2) st 1 < b₂ .. b₁ & b₂ in rng b₁ holds
(b₁ /. 1) .. (Rotate b₁,b₂) = ((len b₁) + 1) - (b₂ .. b₁)

proof end;

theorem Th10: :: SPRECT_5:10

for b₁ being standard non constant special_circular_sequence
for b₂, b₃ being Point of (TOP-REAL 2) st b₂ in rng b₁ & b₃ in rng b₁ & b₂ .. b₁ < b₃ .. b₁ holds
b₂ .. (Rotate b₁,b₃) = ((len b₁) + (b₂ .. b₁)) - (b₃ .. b₁)

proof end;

theorem Th11: :: SPRECT_5:11

for b₁ being standard non constant special_circular_sequence
for b₂, b₃, b₄ being Point of (TOP-REAL 2) st b₂ in rng b₁ & b₃ in rng b₁ & b₄ in rng b₁ & b₂ .. b₁ < b₃ .. b₁ & b₃ .. b₁ < b₄ .. b₁ holds
b₄ .. (Rotate b₁,b₃) < b₂ .. (Rotate b₁,b₃)

proof end;

theorem Th12: :: SPRECT_5:12

for b₁ being standard non constant special_circular_sequence
for b₂, b₃, b₄ being Point of (TOP-REAL 2) st b₂ in rng b₁ & b₃ in rng b₁ & b₄ in rng b₁ & b₂ .. b₁ < b₃ .. b₁ & b₃ .. b₁ < b₄ .. b₁ holds
b₂ .. (Rotate b₁,b₄) < b₃ .. (Rotate b₁,b₄)

proof end;

theorem Th13: :: SPRECT_5:13

for b₁ being standard non constant special_circular_sequence
for b₂, b₃, b₄ being Point of (TOP-REAL 2) st b₂ in rng b₁ & b₃ in rng b₁ & b₄ in rng b₁ & b₂ .. b₁ <= b₃ .. b₁ & b₃ .. b₁ < b₄ .. b₁ holds
b₂ .. (Rotate b₁,b₄) <= b₃ .. (Rotate b₁,b₄)

proof end;

theorem Th14: :: SPRECT_5:14

for b₁ being standard non constant special_circular_sequence holds (S-min (L~ b₁)) .. b₁ < len b₁

proof end;

theorem Th15: :: SPRECT_5:15

for b₁ being standard non constant special_circular_sequence holds (S-max (L~ b₁)) .. b₁ < len b₁

proof end;

theorem Th16: :: SPRECT_5:16

for b₁ being standard non constant special_circular_sequence holds (E-min (L~ b₁)) .. b₁ < len b₁

proof end;

theorem Th17: :: SPRECT_5:17

for b₁ being standard non constant special_circular_sequence holds (E-max (L~ b₁)) .. b₁ < len b₁

proof end;

theorem Th18: :: SPRECT_5:18

for b₁ being standard non constant special_circular_sequence holds (N-min (L~ b₁)) .. b₁ < len b₁

proof end;

theorem Th19: :: SPRECT_5:19

for b₁ being standard non constant special_circular_sequence holds (N-max (L~ b₁)) .. b₁ < len b₁

proof end;

theorem Th20: :: SPRECT_5:20

for b₁ being standard non constant special_circular_sequence holds (W-max (L~ b₁)) .. b₁ < len b₁

proof end;

theorem Th21: :: SPRECT_5:21

for b₁ being standard non constant special_circular_sequence holds (W-min (L~ b₁)) .. b₁ < len b₁

proof end;

Lemma12: for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = N-min (L~ b₁) holds
(E-max (L~ b₁)) .. b₁ < (S-max (L~ b₁)) .. b₁

proof end;

Lemma13: for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = N-min (L~ b₁) holds
(E-max (L~ b₁)) .. b₁ < (S-min (L~ b₁)) .. b₁

proof end;

Lemma14: for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = N-min (L~ b₁) holds
(E-max (L~ b₁)) .. b₁ < (W-min (L~ b₁)) .. b₁

proof end;

Lemma15: for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = N-min (L~ b₁) holds
(E-min (L~ b₁)) .. b₁ < (S-min (L~ b₁)) .. b₁

proof end;

Lemma16: for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = N-min (L~ b₁) holds
(E-min (L~ b₁)) .. b₁ < (W-min (L~ b₁)) .. b₁

proof end;

Lemma17: for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = N-min (L~ b₁) holds
(S-max (L~ b₁)) .. b₁ < (W-min (L~ b₁)) .. b₁

proof end;

Lemma18: for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = N-min (L~ b₁) holds
(N-max (L~ b₁)) .. b₁ < (W-min (L~ b₁)) .. b₁

proof end;

Lemma19: for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = N-min (L~ b₁) holds
(N-min (L~ b₁)) .. b₁ < (W-min (L~ b₁)) .. b₁

proof end;

Lemma20: for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = N-min (L~ b₁) holds
(N-max (L~ b₁)) .. b₁ < (S-max (L~ b₁)) .. b₁

proof end;

Lemma21: for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = N-min (L~ b₁) holds
(N-max (L~ b₁)) .. b₁ < (S-min (L~ b₁)) .. b₁

proof end;

theorem Th22: :: SPRECT_5:22

for b₁ being standard non constant special_circular_sequence st b₁ /. 1 = W-min (L~ b₁) holds
(W-min (L~ b₁)) .. b₁ < (W-max (L~ b₁)) .. b₁

proof end;

theorem Th23: :: SPRECT_5:23

for b₁ being standard non constant special_circular_sequence st b₁ /. 1 = W-min (L~ b₁) holds
(W-max (L~ b₁)) .. b₁ > 1

proof end;

theorem Th24: :: SPRECT_5:24

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = W-min (L~ b₁) & W-max (L~ b₁) <> N-min (L~ b₁) holds
(W-max (L~ b₁)) .. b₁ < (N-min (L~ b₁)) .. b₁

proof end;

theorem Th25: :: SPRECT_5:25

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = W-min (L~ b₁) holds
(N-min (L~ b₁)) .. b₁ < (N-max (L~ b₁)) .. b₁

proof end;

theorem Th26: :: SPRECT_5:26

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = W-min (L~ b₁) & N-max (L~ b₁) <> E-max (L~ b₁) holds
(N-max (L~ b₁)) .. b₁ < (E-max (L~ b₁)) .. b₁

proof end;

theorem Th27: :: SPRECT_5:27

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = W-min (L~ b₁) holds
(E-max (L~ b₁)) .. b₁ < (E-min (L~ b₁)) .. b₁

proof end;

theorem Th28: :: SPRECT_5:28

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = W-min (L~ b₁) & E-min (L~ b₁) <> S-max (L~ b₁) holds
(E-min (L~ b₁)) .. b₁ < (S-max (L~ b₁)) .. b₁

proof end;

theorem Th29: :: SPRECT_5:29

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = W-min (L~ b₁) & S-min (L~ b₁) <> W-min (L~ b₁) holds
(S-max (L~ b₁)) .. b₁ < (S-min (L~ b₁)) .. b₁

proof end;

theorem Th30: :: SPRECT_5:30

for b₁ being standard non constant special_circular_sequence st b₁ /. 1 = S-max (L~ b₁) holds
(S-max (L~ b₁)) .. b₁ < (S-min (L~ b₁)) .. b₁

proof end;

theorem Th31: :: SPRECT_5:31

for b₁ being standard non constant special_circular_sequence st b₁ /. 1 = S-max (L~ b₁) holds
(S-min (L~ b₁)) .. b₁ > 1

proof end;

Lemma29: for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = W-min (L~ b₁) holds
(E-max (L~ b₁)) .. b₁ < (S-max (L~ b₁)) .. b₁

proof end;

Lemma30: for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = W-min (L~ b₁) holds
(N-min (L~ b₁)) .. b₁ < (E-max (L~ b₁)) .. b₁

proof end;

Lemma31: for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = W-min (L~ b₁) holds
(N-min (L~ b₁)) .. b₁ < (S-max (L~ b₁)) .. b₁

proof end;

Lemma32: for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = W-min (L~ b₁) holds
(N-max (L~ b₁)) .. b₁ < (S-max (L~ b₁)) .. b₁

proof end;

Lemma33: for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = W-min (L~ b₁) holds
(W-max (L~ b₁)) .. b₁ < (S-max (L~ b₁)) .. b₁

proof end;

Lemma34: for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = W-min (L~ b₁) holds
(N-max (L~ b₁)) .. b₁ < (E-min (L~ b₁)) .. b₁

proof end;

Lemma35: for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = W-min (L~ b₁) holds
(N-min (L~ b₁)) .. b₁ < (E-max (L~ b₁)) .. b₁

proof end;

Lemma36: for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = W-min (L~ b₁) holds
(W-max (L~ b₁)) .. b₁ < (E-max (L~ b₁)) .. b₁

proof end;

Lemma37: for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = W-min (L~ b₁) holds
(W-max (L~ b₁)) .. b₁ < (E-min (L~ b₁)) .. b₁

proof end;

theorem Th32: :: SPRECT_5:32

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = S-max (L~ b₁) & S-min (L~ b₁) <> W-min (L~ b₁) holds
(S-min (L~ b₁)) .. b₁ < (W-min (L~ b₁)) .. b₁

proof end;

theorem Th33: :: SPRECT_5:33

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = S-max (L~ b₁) holds
(W-min (L~ b₁)) .. b₁ < (W-max (L~ b₁)) .. b₁

proof end;

theorem Th34: :: SPRECT_5:34

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = S-max (L~ b₁) & W-max (L~ b₁) <> N-min (L~ b₁) holds
(W-max (L~ b₁)) .. b₁ < (N-min (L~ b₁)) .. b₁

proof end;

theorem Th35: :: SPRECT_5:35

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = S-max (L~ b₁) holds
(N-min (L~ b₁)) .. b₁ < (N-max (L~ b₁)) .. b₁

proof end;

theorem Th36: :: SPRECT_5:36

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = S-max (L~ b₁) & N-max (L~ b₁) <> E-max (L~ b₁) holds
(N-max (L~ b₁)) .. b₁ < (E-max (L~ b₁)) .. b₁

proof end;

theorem Th37: :: SPRECT_5:37

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = S-max (L~ b₁) & E-min (L~ b₁) <> S-max (L~ b₁) holds
(E-max (L~ b₁)) .. b₁ < (E-min (L~ b₁)) .. b₁

proof end;

theorem Th38: :: SPRECT_5:38

for b₁ being standard non constant special_circular_sequence st b₁ /. 1 = E-max (L~ b₁) holds
(E-max (L~ b₁)) .. b₁ < (E-min (L~ b₁)) .. b₁

proof end;

theorem Th39: :: SPRECT_5:39

for b₁ being standard non constant special_circular_sequence st b₁ /. 1 = E-max (L~ b₁) holds
(E-min (L~ b₁)) .. b₁ > 1

proof end;

theorem Th40: :: SPRECT_5:40

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = E-max (L~ b₁) & S-max (L~ b₁) <> E-min (L~ b₁) holds
(E-min (L~ b₁)) .. b₁ < (S-max (L~ b₁)) .. b₁

proof end;

theorem Th41: :: SPRECT_5:41

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = E-max (L~ b₁) holds
(S-max (L~ b₁)) .. b₁ < (S-min (L~ b₁)) .. b₁

proof end;

Lemma46: for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = S-max (L~ b₁) holds
(N-min (L~ b₁)) .. b₁ < (E-max (L~ b₁)) .. b₁

proof end;

Lemma47: for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = S-max (L~ b₁) holds
(W-max (L~ b₁)) .. b₁ < (E-max (L~ b₁)) .. b₁

proof end;

Lemma48: for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = S-max (L~ b₁) holds
(W-min (L~ b₁)) .. b₁ < (E-max (L~ b₁)) .. b₁

proof end;

Lemma49: for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = S-max (L~ b₁) holds
(W-max (L~ b₁)) .. b₁ < (N-max (L~ b₁)) .. b₁

proof end;

Lemma50: for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = S-max (L~ b₁) holds
(W-min (L~ b₁)) .. b₁ < (N-min (L~ b₁)) .. b₁

proof end;

Lemma51: for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = S-max (L~ b₁) holds
(S-min (L~ b₁)) .. b₁ < (N-min (L~ b₁)) .. b₁

proof end;

Lemma52: for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = S-max (L~ b₁) holds
(S-min (L~ b₁)) .. b₁ < (N-max (L~ b₁)) .. b₁

proof end;

theorem Th42: :: SPRECT_5:42

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = E-max (L~ b₁) & S-min (L~ b₁) <> W-min (L~ b₁) holds
(S-min (L~ b₁)) .. b₁ < (W-min (L~ b₁)) .. b₁

proof end;

theorem Th43: :: SPRECT_5:43

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = E-max (L~ b₁) holds
(W-min (L~ b₁)) .. b₁ < (W-max (L~ b₁)) .. b₁

proof end;

theorem Th44: :: SPRECT_5:44

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = E-max (L~ b₁) & W-max (L~ b₁) <> N-min (L~ b₁) holds
(W-max (L~ b₁)) .. b₁ < (N-min (L~ b₁)) .. b₁

proof end;

theorem Th45: :: SPRECT_5:45

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = E-max (L~ b₁) & N-max (L~ b₁) <> E-max (L~ b₁) holds
(N-min (L~ b₁)) .. b₁ < (N-max (L~ b₁)) .. b₁

proof end;

theorem Th46: :: SPRECT_5:46

for b₁ being standard non constant special_circular_sequence st b₁ /. 1 = N-max (L~ b₁) & N-max (L~ b₁) <> E-max (L~ b₁) holds
(N-max (L~ b₁)) .. b₁ < (E-max (L~ b₁)) .. b₁

proof end;

theorem Th47: :: SPRECT_5:47

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = N-max (L~ b₁) holds
(E-max (L~ b₁)) .. b₁ < (E-min (L~ b₁)) .. b₁

proof end;

theorem Th48: :: SPRECT_5:48

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = N-max (L~ b₁) & E-min (L~ b₁) <> S-max (L~ b₁) holds
(E-min (L~ b₁)) .. b₁ < (S-max (L~ b₁)) .. b₁

proof end;

theorem Th49: :: SPRECT_5:49

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = N-max (L~ b₁) holds
(S-max (L~ b₁)) .. b₁ < (S-min (L~ b₁)) .. b₁

proof end;

theorem Th50: :: SPRECT_5:50

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = N-max (L~ b₁) & S-min (L~ b₁) <> W-min (L~ b₁) holds
(S-min (L~ b₁)) .. b₁ < (W-min (L~ b₁)) .. b₁

proof end;

theorem Th51: :: SPRECT_5:51

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = N-max (L~ b₁) holds
(W-min (L~ b₁)) .. b₁ < (W-max (L~ b₁)) .. b₁

proof end;

theorem Th52: :: SPRECT_5:52

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = N-max (L~ b₁) & N-min (L~ b₁) <> W-max (L~ b₁) holds
(W-max (L~ b₁)) .. b₁ < (N-min (L~ b₁)) .. b₁

proof end;

theorem Th53: :: SPRECT_5:53

for b₁ being standard non constant special_circular_sequence st b₁ /. 1 = E-min (L~ b₁) & E-min (L~ b₁) <> S-max (L~ b₁) holds
(E-min (L~ b₁)) .. b₁ < (S-max (L~ b₁)) .. b₁

proof end;

theorem Th54: :: SPRECT_5:54

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = E-min (L~ b₁) holds
(S-max (L~ b₁)) .. b₁ < (S-min (L~ b₁)) .. b₁

proof end;

theorem Th55: :: SPRECT_5:55

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = E-min (L~ b₁) & S-min (L~ b₁) <> W-min (L~ b₁) holds
(S-min (L~ b₁)) .. b₁ < (W-min (L~ b₁)) .. b₁

proof end;

Lemma56: for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = E-max (L~ b₁) holds
(S-max (L~ b₁)) .. b₁ < (W-min (L~ b₁)) .. b₁

proof end;

Lemma57: for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = E-max (L~ b₁) holds
(E-min (L~ b₁)) .. b₁ < (W-min (L~ b₁)) .. b₁

proof end;

Lemma58: for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = E-max (L~ b₁) holds
(E-min (L~ b₁)) .. b₁ < (W-max (L~ b₁)) .. b₁

proof end;

Lemma59: for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = E-max (L~ b₁) holds
(S-min (L~ b₁)) .. b₁ < (W-max (L~ b₁)) .. b₁

proof end;

theorem Th56: :: SPRECT_5:56

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = E-min (L~ b₁) holds
(W-min (L~ b₁)) .. b₁ < (W-max (L~ b₁)) .. b₁

proof end;

theorem Th57: :: SPRECT_5:57

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = E-min (L~ b₁) & W-max (L~ b₁) <> N-min (L~ b₁) holds
(W-max (L~ b₁)) .. b₁ < (N-min (L~ b₁)) .. b₁

proof end;

theorem Th58: :: SPRECT_5:58

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = E-min (L~ b₁) holds
(N-min (L~ b₁)) .. b₁ < (N-max (L~ b₁)) .. b₁

proof end;

theorem Th59: :: SPRECT_5:59

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = E-min (L~ b₁) & E-max (L~ b₁) <> N-max (L~ b₁) holds
(N-max (L~ b₁)) .. b₁ < (E-max (L~ b₁)) .. b₁

proof end;

theorem Th60: :: SPRECT_5:60

for b₁ being standard non constant special_circular_sequence st b₁ /. 1 = S-min (L~ b₁) & S-min (L~ b₁) <> W-min (L~ b₁) holds
(S-min (L~ b₁)) .. b₁ < (W-min (L~ b₁)) .. b₁

proof end;

theorem Th61: :: SPRECT_5:61

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = S-min (L~ b₁) holds
(W-min (L~ b₁)) .. b₁ < (W-max (L~ b₁)) .. b₁

proof end;

theorem Th62: :: SPRECT_5:62

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = S-min (L~ b₁) & W-max (L~ b₁) <> N-min (L~ b₁) holds
(W-max (L~ b₁)) .. b₁ < (N-min (L~ b₁)) .. b₁

proof end;

theorem Th63: :: SPRECT_5:63

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = S-min (L~ b₁) holds
(N-min (L~ b₁)) .. b₁ < (N-max (L~ b₁)) .. b₁

proof end;

theorem Th64: :: SPRECT_5:64

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = S-min (L~ b₁) & N-max (L~ b₁) <> E-max (L~ b₁) holds
(N-max (L~ b₁)) .. b₁ < (E-max (L~ b₁)) .. b₁

proof end;

theorem Th65: :: SPRECT_5:65

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = S-min (L~ b₁) holds
(E-max (L~ b₁)) .. b₁ < (E-min (L~ b₁)) .. b₁

proof end;

theorem Th66: :: SPRECT_5:66

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = S-min (L~ b₁) & S-max (L~ b₁) <> E-min (L~ b₁) holds
(E-min (L~ b₁)) .. b₁ < (S-max (L~ b₁)) .. b₁

proof end;

theorem Th67: :: SPRECT_5:67

for b₁ being standard non constant special_circular_sequence st b₁ /. 1 = W-max (L~ b₁) & W-max (L~ b₁) <> N-min (L~ b₁) holds
(W-max (L~ b₁)) .. b₁ < (N-min (L~ b₁)) .. b₁

proof end;

theorem Th68: :: SPRECT_5:68

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = W-max (L~ b₁) holds
(N-min (L~ b₁)) .. b₁ < (N-max (L~ b₁)) .. b₁

proof end;

theorem Th69: :: SPRECT_5:69

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = W-max (L~ b₁) & N-max (L~ b₁) <> E-max (L~ b₁) holds
(N-max (L~ b₁)) .. b₁ < (E-max (L~ b₁)) .. b₁

proof end;

theorem Th70: :: SPRECT_5:70

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = W-max (L~ b₁) holds
(E-max (L~ b₁)) .. b₁ < (E-min (L~ b₁)) .. b₁

proof end;

theorem Th71: :: SPRECT_5:71

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = W-max (L~ b₁) & E-min (L~ b₁) <> S-max (L~ b₁) holds
(E-min (L~ b₁)) .. b₁ < (S-max (L~ b₁)) .. b₁

proof end;

theorem Th72: :: SPRECT_5:72

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = W-max (L~ b₁) holds
(S-max (L~ b₁)) .. b₁ < (S-min (L~ b₁)) .. b₁

proof end;

theorem Th73: :: SPRECT_5:73

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = W-max (L~ b₁) & W-min (L~ b₁) <> S-min (L~ b₁) holds
(S-min (L~ b₁)) .. b₁ < (W-min (L~ b₁)) .. b₁

proof end;