:: SPRECT_2 semantic presentation

theorem Th1: :: SPRECT_2:1

for b₁, b₂, b₃, b₄ being set st b₁ /\ b₂ c= {b₄} & b₄ in b₃ & b₃ misses b₂ holds
b₁ \/ b₃ misses b₂

proof end;

theorem Th2: :: SPRECT_2:2

for b₁, b₂, b₃, b₄ being set st b₁ /\ b₃ = {b₄} & b₄ in b₂ & b₂ c= b₃ holds
b₁ /\ b₂ = {b₄}

proof end;

theorem Th3: :: SPRECT_2:3

canceled;

theorem Th4: :: SPRECT_2:4

for b₁, b₂ being set st ( for b₃, b₄ being set st b₃ in b₁ & b₄ in b₂ holds
b₃ misses b₄ ) holds
union b₁ misses union b₂

proof end;

theorem Th5: :: SPRECT_2:5

for b₁, b₂, b₃ being Nat
for b₄ being non empty set
for b₅ being FinSequence of b₄ st b₁ <= b₂ & b₁ in dom b₅ & b₂ in dom b₅ & b₃ in dom (mid b₅,b₁,b₂) holds
(b₃ + b₁) -' 1 in dom b₅

proof end;

theorem Th6: :: SPRECT_2:6

for b₁, b₂, b₃ being Nat
for b₄ being non empty set
for b₅ being FinSequence of b₄ st b₁ > b₂ & b₁ in dom b₅ & b₂ in dom b₅ & b₃ in dom (mid b₅,b₁,b₂) holds
(b₁ -' b₃) + 1 in dom b₅

proof end;

theorem Th7: :: SPRECT_2:7

for b₁, b₂, b₃ being Nat
for b₄ being non empty set
for b₅ being FinSequence of b₄ st b₁ <= b₂ & b₁ in dom b₅ & b₂ in dom b₅ & b₃ in dom (mid b₅,b₁,b₂) holds
(mid b₅,b₁,b₂) /. b₃ = b₅ /. ((b₃ + b₁) -' 1)

proof end;

theorem Th8: :: SPRECT_2:8

for b₁, b₂, b₃ being Nat
for b₄ being non empty set
for b₅ being FinSequence of b₄ st b₁ > b₂ & b₁ in dom b₅ & b₂ in dom b₅ & b₃ in dom (mid b₅,b₁,b₂) holds
(mid b₅,b₁,b₂) /. b₃ = b₅ /. ((b₁ -' b₃) + 1)

proof end;

theorem Th9: :: SPRECT_2:9

for b₁, b₂ being Nat
for b₃ being non empty set
for b₄ being FinSequence of b₃ st b₁ in dom b₄ & b₂ in dom b₄ holds
len (mid b₄,b₁,b₂) >= 1

proof end;

theorem Th10: :: SPRECT_2:10

for b₁, b₂ being Nat
for b₃ being non empty set
for b₄ being FinSequence of b₃ st b₁ in dom b₄ & b₂ in dom b₄ & len (mid b₄,b₁,b₂) = 1 holds
b₁ = b₂

proof end;

theorem Th11: :: SPRECT_2:11

for b₁, b₂ being Nat
for b₃ being non empty set
for b₄ being FinSequence of b₃ st b₁ in dom b₄ & b₂ in dom b₄ holds
not mid b₄,b₁,b₂ is empty

proof end;

theorem Th12: :: SPRECT_2:12

for b₁, b₂ being Nat
for b₃ being non empty set
for b₄ being FinSequence of b₃ st b₁ in dom b₄ & b₂ in dom b₄ holds
(mid b₄,b₁,b₂) /. 1 = b₄ /. b₁

proof end;

theorem Th13: :: SPRECT_2:13

for b₁, b₂ being Nat
for b₃ being non empty set
for b₄ being FinSequence of b₃ st b₁ in dom b₄ & b₂ in dom b₄ holds
(mid b₄,b₁,b₂) /. (len (mid b₄,b₁,b₂)) = b₄ /. b₂

proof end;

theorem Th14: :: SPRECT_2:14

for b₁ being compact Subset of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₂ in b₁ & b₂ `2 = N-bound b₁ holds
b₂ in N-most b₁

proof end;

theorem Th15: :: SPRECT_2:15

for b₁ being compact Subset of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₂ in b₁ & b₂ `2 = S-bound b₁ holds
b₂ in S-most b₁

proof end;

theorem Th16: :: SPRECT_2:16

for b₁ being compact Subset of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₂ in b₁ & b₂ `1 = W-bound b₁ holds
b₂ in W-most b₁

proof end;

theorem Th17: :: SPRECT_2:17

for b₁ being compact Subset of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₂ in b₁ & b₂ `1 = E-bound b₁ holds
b₂ in E-most b₁

proof end;

theorem Th18: :: SPRECT_2:18

for b₁, b₂ being Nat
for b₃ being FinSequence of (TOP-REAL 2) st 1 <= b₁ & b₁ <= b₂ & b₂ <= len b₃ holds
L~ (mid b₃,b₁,b₂) = union { (LSeg b₃,b₄) where B is Nat : ( b₁ <= b₄ & b₄ < b₂ ) }

proof end;

theorem Th19: :: SPRECT_2:19

for b₁ being FinSequence of (TOP-REAL 2) holds dom (X_axis b₁) = dom b₁

proof end;

theorem Th20: :: SPRECT_2:20

for b₁ being FinSequence of (TOP-REAL 2) holds dom (Y_axis b₁) = dom b₁

proof end;

theorem Th21: :: SPRECT_2:21

for b₁, b₂, b₃ being Point of (TOP-REAL 2) st b₂ in LSeg b₁,b₃ & b₁ `1 <= b₂ `1 & b₃ `1 <= b₂ `1 & not b₁ = b₂ & not b₂ = b₃ holds
( b₁ `1 = b₂ `1 & b₃ `1 = b₂ `1 )

proof end;

theorem Th22: :: SPRECT_2:22

for b₁, b₂, b₃ being Point of (TOP-REAL 2) st b₂ in LSeg b₁,b₃ & b₁ `2 <= b₂ `2 & b₃ `2 <= b₂ `2 & not b₁ = b₂ & not b₂ = b₃ holds
( b₁ `2 = b₂ `2 & b₃ `2 = b₂ `2 )

proof end;

theorem Th23: :: SPRECT_2:23

for b₁, b₂, b₃ being Point of (TOP-REAL 2) st b₂ in LSeg b₁,b₃ & b₁ `1 >= b₂ `1 & b₃ `1 >= b₂ `1 & not b₁ = b₂ & not b₂ = b₃ holds
( b₁ `1 = b₂ `1 & b₃ `1 = b₂ `1 )

proof end;

theorem Th24: :: SPRECT_2:24

for b₁, b₂, b₃ being Point of (TOP-REAL 2) st b₂ in LSeg b₁,b₃ & b₁ `2 >= b₂ `2 & b₃ `2 >= b₂ `2 & not b₁ = b₂ & not b₂ = b₃ holds
( b₁ `2 = b₂ `2 & b₃ `2 = b₂ `2 )

proof end;

definition

let c₁, c₂ be FinSequence of (TOP-REAL 2);
pred c₂ is_in_the_area_of c₁ means :Def1: :: SPRECT_2:def 1
for b₁ being Nat st b₁ in dom a₂ holds
( W-bound (L~ a₁) <= (a₂ /. b₁) `1 & (a₂ /. b₁) `1 <= E-bound (L~ a₁) & S-bound (L~ a₁) <= (a₂ /. b₁) `2 & (a₂ /. b₁) `2 <= N-bound (L~ a₁) );

end;

:: deftheorem Def1 defines is_in_the_area_of SPRECT_2:def 1 :

theorem Th25: :: SPRECT_2:25

for b₁ being non trivial FinSequence of (TOP-REAL 2) holds b₁ is_in_the_area_of b₁

proof end;

theorem Th26: :: SPRECT_2:26

for b₁, b₂ being FinSequence of (TOP-REAL 2) st b₂ is_in_the_area_of b₁ holds
for b₃, b₄ being Nat st b₃ in dom b₂ & b₄ in dom b₂ holds
mid b₂,b₃,b₄ is_in_the_area_of b₁

proof end;

theorem Th27: :: SPRECT_2:27

for b₁ being non trivial FinSequence of (TOP-REAL 2)
for b₂, b₃ being Nat st b₂ in dom b₁ & b₃ in dom b₁ holds
mid b₁,b₂,b₃ is_in_the_area_of b₁

proof end;

theorem Th28: :: SPRECT_2:28

for b₁, b₂, b₃ being FinSequence of (TOP-REAL 2) st b₂ is_in_the_area_of b₁ & b₃ is_in_the_area_of b₁ holds
b₂ ^ b₃ is_in_the_area_of b₁

proof end;

theorem Th29: :: SPRECT_2:29

for b₁ being non trivial FinSequence of (TOP-REAL 2) holds <*(NE-corner (L~ b₁))*> is_in_the_area_of b₁

proof end;

theorem Th30: :: SPRECT_2:30

for b₁ being non trivial FinSequence of (TOP-REAL 2) holds <*(NW-corner (L~ b₁))*> is_in_the_area_of b₁

proof end;

theorem Th31: :: SPRECT_2:31

for b₁ being non trivial FinSequence of (TOP-REAL 2) holds <*(SE-corner (L~ b₁))*> is_in_the_area_of b₁

proof end;

theorem Th32: :: SPRECT_2:32

for b₁ being non trivial FinSequence of (TOP-REAL 2) holds <*(SW-corner (L~ b₁))*> is_in_the_area_of b₁

proof end;

definition

let c₁, c₂ be FinSequence of (TOP-REAL 2);
pred c₂ is_a_h.c._for c₁ means :Def2: :: SPRECT_2:def 2
( a₂ is_in_the_area_of a₁ & (a₂ /. 1) `1 = W-bound (L~ a₁) & (a₂ /. (len a₂)) `1 = E-bound (L~ a₁) );
pred c₂ is_a_v.c._for c₁ means :Def3: :: SPRECT_2:def 3
( a₂ is_in_the_area_of a₁ & (a₂ /. 1) `2 = S-bound (L~ a₁) & (a₂ /. (len a₂)) `2 = N-bound (L~ a₁) );

end;

:: deftheorem Def2 defines is_a_h.c._for SPRECT_2:def 2 :

:: deftheorem Def3 defines is_a_v.c._for SPRECT_2:def 3 :

theorem Th33: :: SPRECT_2:33

for b₁ being FinSequence of (TOP-REAL 2)
for b₂, b₃ being one-to-one special FinSequence of (TOP-REAL 2) st 2 <= len b₂ & 2 <= len b₃ & b₂ is_a_h.c._for b₁ & b₃ is_a_v.c._for b₁ holds
L~ b₂ meets L~ b₃

proof end;

definition

let c₁ be FinSequence of (TOP-REAL 2);
attr a₁ is clockwise_oriented means :Def4: :: SPRECT_2:def 4
(Rotate a₁,(N-min (L~ a₁))) /. 2 in N-most (L~ a₁);

end;

:: deftheorem Def4 defines clockwise_oriented SPRECT_2:def 4 :

theorem Th34: :: SPRECT_2:34

for b₁ being standard non constant special_circular_sequence st b₁ /. 1 = N-min (L~ b₁) holds
( b₁ is clockwise_oriented iff b₁ /. 2 in N-most (L~ b₁) )

proof end;

registration

cluster R^2-unit_square -> compact ;
coherence by TOPREAL2:2;

end;

theorem Th35: :: SPRECT_2:35

N-bound R^2-unit_square = 1

proof end;

theorem Th36: :: SPRECT_2:36

W-bound R^2-unit_square = 0

proof end;

theorem Th37: :: SPRECT_2:37

E-bound R^2-unit_square = 1

proof end;

theorem Th38: :: SPRECT_2:38

S-bound R^2-unit_square = 0

proof end;

Lemma41: NW-corner R^2-unit_square = |[0,1]|
by Th35, Th36, PSCOMP_1:def 35;

Lemma42: NE-corner R^2-unit_square = |[1,1]|
by Th35, Th37, PSCOMP_1:def 36;

theorem Th39: :: SPRECT_2:39

N-most R^2-unit_square = LSeg |[0,1]|,|[1,1]|

proof end;

theorem Th40: :: SPRECT_2:40

N-min R^2-unit_square = |[0,1]|

proof end;

registration

let c₁ be non empty non horizontal non vertical compact Subset of (TOP-REAL 2);
cluster SpStSeq a₁ -> clockwise_oriented ;
coherence

proof end;

end;

registration

cluster standard non constant clockwise_oriented FinSequence of the carrier of (TOP-REAL 2);
existence

proof end;

end;

theorem Th41: :: SPRECT_2:41

for b₁ being standard non constant special_circular_sequence
for b₂, b₃ being Nat st b₂ > b₃ & ( ( 1 < b₃ & b₂ <= len b₁ ) or ( 1 <= b₃ & b₂ < len b₁ ) ) holds
mid b₁,b₂,b₃ is S-Sequence_in_R2

proof end;

theorem Th42: :: SPRECT_2:42

for b₁ being standard non constant special_circular_sequence
for b₂, b₃ being Nat st b₂ < b₃ & ( ( 1 < b₂ & b₃ <= len b₁ ) or ( 1 <= b₂ & b₃ < len b₁ ) ) holds
mid b₁,b₂,b₃ is S-Sequence_in_R2

proof end;

theorem Th43: :: SPRECT_2:43

for b₁ being non trivial FinSequence of (TOP-REAL 2) holds N-min (L~ b₁) in rng b₁

proof end;

theorem Th44: :: SPRECT_2:44

for b₁ being non trivial FinSequence of (TOP-REAL 2) holds N-max (L~ b₁) in rng b₁

proof end;

theorem Th45: :: SPRECT_2:45

for b₁ being non trivial FinSequence of (TOP-REAL 2) holds S-min (L~ b₁) in rng b₁

proof end;

theorem Th46: :: SPRECT_2:46

for b₁ being non trivial FinSequence of (TOP-REAL 2) holds S-max (L~ b₁) in rng b₁

proof end;

theorem Th47: :: SPRECT_2:47

for b₁ being non trivial FinSequence of (TOP-REAL 2) holds W-min (L~ b₁) in rng b₁

proof end;

theorem Th48: :: SPRECT_2:48

for b₁ being non trivial FinSequence of (TOP-REAL 2) holds W-max (L~ b₁) in rng b₁

proof end;

theorem Th49: :: SPRECT_2:49

for b₁ being non trivial FinSequence of (TOP-REAL 2) holds E-min (L~ b₁) in rng b₁

proof end;

theorem Th50: :: SPRECT_2:50

for b₁ being non trivial FinSequence of (TOP-REAL 2) holds E-max (L~ b₁) in rng b₁

proof end;

theorem Th51: :: SPRECT_2:51

for b₁, b₂, b₃, b₄ being Nat
for b₅ being standard non constant special_circular_sequence st 1 <= b₁ & b₁ <= b₂ & b₂ < b₃ & b₃ <= b₄ & b₄ <= len b₅ & ( 1 < b₁ or b₄ < len b₅ ) holds
L~ (mid b₅,b₁,b₂) misses L~ (mid b₅,b₃,b₄)

proof end;

theorem Th52: :: SPRECT_2:52

proof end;

theorem Th53: :: SPRECT_2:53

for b₁, b₂, b₃, b₄ being Nat
for b₅ being standard non constant special_circular_sequence st 1 <= b₁ & b₁ <= b₂ & b₂ < b₃ & b₃ <= b₄ & b₄ <= len b₅ & ( 1 < b₁ or b₄ < len b₅ ) holds
L~ (mid b₅,b₂,b₁) misses L~ (mid b₅,b₄,b₃)

proof end;

theorem Th54: :: SPRECT_2:54

proof end;

theorem Th55: :: SPRECT_2:55

for b₁ being standard non constant special_circular_sequence holds (N-min (L~ b₁)) `1 < (N-max (L~ b₁)) `1

proof end;

theorem Th56: :: SPRECT_2:56

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

proof end;

theorem Th57: :: SPRECT_2:57

for b₁ being standard non constant special_circular_sequence holds (E-min (L~ b₁)) `2 < (E-max (L~ b₁)) `2

proof end;

theorem Th58: :: SPRECT_2:58

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

proof end;

theorem Th59: :: SPRECT_2:59

for b₁ being standard non constant special_circular_sequence holds (S-min (L~ b₁)) `1 < (S-max (L~ b₁)) `1

proof end;

theorem Th60: :: SPRECT_2:60

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

proof end;

theorem Th61: :: SPRECT_2:61

for b₁ being standard non constant special_circular_sequence holds (W-min (L~ b₁)) `2 < (W-max (L~ b₁)) `2

proof end;

theorem Th62: :: SPRECT_2:62

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

proof end;

theorem Th63: :: SPRECT_2:63

for b₁ being standard non constant special_circular_sequence holds LSeg (NW-corner (L~ b₁)),(N-min (L~ b₁)) misses LSeg (N-max (L~ b₁)),(NE-corner (L~ b₁))

proof end;

theorem Th64: :: SPRECT_2:64

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₁ is_S-Seq & b₂ <> b₁ /. 1 & ( b₂ `1 = (b₁ /. 1) `1 or b₂ `2 = (b₁ /. 1) `2 ) & (LSeg b₂,(b₁ /. 1)) /\ (L~ b₁) = {(b₁ /. 1)} holds
<*b₂*> ^ b₁ is S-Sequence_in_R2

proof end;

theorem Th65: :: SPRECT_2:65

for b₁ being FinSequence of (TOP-REAL 2)
for b₂ being Point of (TOP-REAL 2) st b₁ is_S-Seq & b₂ <> b₁ /. (len b₁) & ( b₂ `1 = (b₁ /. (len b₁)) `1 or b₂ `2 = (b₁ /. (len b₁)) `2 ) & (LSeg b₂,(b₁ /. (len b₁))) /\ (L~ b₁) = {(b₁ /. (len b₁))} holds
b₁ ^ <*b₂*> is S-Sequence_in_R2

proof end;

theorem Th66: :: SPRECT_2:66

for b₁ being standard non constant special_circular_sequence
for b₂, b₃ being Nat st b₂ in dom b₁ & b₃ in dom b₁ & mid b₁,b₂,b₃ is S-Sequence_in_R2 & b₁ /. b₃ = N-max (L~ b₁) & N-max (L~ b₁) <> NE-corner (L~ b₁) holds
(mid b₁,b₂,b₃) ^ <*(NE-corner (L~ b₁))*> is S-Sequence_in_R2

proof end;

theorem Th67: :: SPRECT_2:67

for b₁ being standard non constant special_circular_sequence
for b₂, b₃ being Nat st b₂ in dom b₁ & b₃ in dom b₁ & mid b₁,b₂,b₃ is S-Sequence_in_R2 & b₁ /. b₃ = E-max (L~ b₁) & E-max (L~ b₁) <> NE-corner (L~ b₁) holds
(mid b₁,b₂,b₃) ^ <*(NE-corner (L~ b₁))*> is S-Sequence_in_R2

proof end;

theorem Th68: :: SPRECT_2:68

for b₁ being standard non constant special_circular_sequence
for b₂, b₃ being Nat st b₂ in dom b₁ & b₃ in dom b₁ & mid b₁,b₂,b₃ is S-Sequence_in_R2 & b₁ /. b₃ = S-max (L~ b₁) & S-max (L~ b₁) <> SE-corner (L~ b₁) holds
(mid b₁,b₂,b₃) ^ <*(SE-corner (L~ b₁))*> is S-Sequence_in_R2

proof end;

theorem Th69: :: SPRECT_2:69

proof end;

theorem Th70: :: SPRECT_2:70

for b₁ being standard non constant special_circular_sequence
for b₂, b₃ being Nat st b₂ in dom b₁ & b₃ in dom b₁ & mid b₁,b₂,b₃ is S-Sequence_in_R2 & b₁ /. b₂ = N-min (L~ b₁) & N-min (L~ b₁) <> NW-corner (L~ b₁) holds
<*(NW-corner (L~ b₁))*> ^ (mid b₁,b₂,b₃) is S-Sequence_in_R2

proof end;

theorem Th71: :: SPRECT_2:71

for b₁ being standard non constant special_circular_sequence
for b₂, b₃ being Nat st b₂ in dom b₁ & b₃ in dom b₁ & mid b₁,b₂,b₃ is S-Sequence_in_R2 & b₁ /. b₂ = W-min (L~ b₁) & W-min (L~ b₁) <> SW-corner (L~ b₁) holds
<*(SW-corner (L~ b₁))*> ^ (mid b₁,b₂,b₃) is S-Sequence_in_R2

proof end;

Lemma73: for b₁ being standard non constant special_circular_sequence
for b₂, b₃ being Nat st b₂ in dom b₁ & b₃ in dom b₁ & mid b₁,b₂,b₃ is S-Sequence_in_R2 & b₁ /. b₂ = N-min (L~ b₁) & N-min (L~ b₁) <> NW-corner (L~ b₁) & b₁ /. b₃ = N-max (L~ b₁) & N-max (L~ b₁) <> NE-corner (L~ b₁) holds
(<*(NW-corner (L~ b₁))*> ^ (mid b₁,b₂,b₃)) ^ <*(NE-corner (L~ b₁))*> is S-Sequence_in_R2

proof end;

registration

let c₁ be standard non constant special_circular_sequence;
cluster L~ a₁ -> being_simple_closed_curve ;
coherence by JORDAN4:63;

end;

Lemma74: for b₁ being standard non constant special_circular_sequence holds LSeg (S-max (L~ b₁)),(SE-corner (L~ b₁)) misses LSeg (NW-corner (L~ b₁)),(N-min (L~ b₁))

proof end;

Lemma75: for b₁ being standard non constant special_circular_sequence
for b₂, b₃ being Nat st b₂ in dom b₁ & b₃ in dom b₁ & mid b₁,b₂,b₃ is S-Sequence_in_R2 & b₁ /. b₂ = N-min (L~ b₁) & N-min (L~ b₁) <> NW-corner (L~ b₁) & b₁ /. b₃ = S-max (L~ b₁) & S-max (L~ b₁) <> SE-corner (L~ b₁) holds
(<*(NW-corner (L~ b₁))*> ^ (mid b₁,b₂,b₃)) ^ <*(SE-corner (L~ b₁))*> is S-Sequence_in_R2

proof end;

theorem Th72: :: SPRECT_2:72

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

proof end;

theorem Th73: :: SPRECT_2:73

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

proof end;

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

proof end;

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

Lemma79: 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 Th74: :: SPRECT_2:74

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

proof end;

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

Lemma81: for b₁ being standard non constant special_circular_sequence holds (LSeg (N-min (L~ b₁)),(NW-corner (L~ b₁))) /\ (LSeg (NE-corner (L~ b₁)),(E-max (L~ b₁))) = {}

proof end;

theorem Th75: :: SPRECT_2:75

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

proof end;

theorem Th76: :: SPRECT_2:76

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = N-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 Th77: :: SPRECT_2:77

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

proof end;

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

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

proof end;

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

theorem Th78: :: SPRECT_2:78

for b₁ being standard non constant clockwise_oriented special_circular_sequence st b₁ /. 1 = N-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 Th79: :: SPRECT_2:79

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

proof end;

theorem Th80: :: SPRECT_2:80

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

proof end;

theorem Th81: :: SPRECT_2:81

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

proof end;