:: by Andrzej Trybulec and Yatsuka Nakamura

::

:: Received November 30, 1997

:: Copyright (c) 1997-2021 Association of Mizar Users

theorem Th1: :: SPRECT_2:1

for i, j, k being Nat

for D being non empty set

for f being FinSequence of D st i <= j & i in dom f & j in dom f & k in dom (mid (f,i,j)) holds

(k + i) -' 1 in dom f

for D being non empty set

for f being FinSequence of D st i <= j & i in dom f & j in dom f & k in dom (mid (f,i,j)) holds

(k + i) -' 1 in dom f

proof end;

theorem Th2: :: SPRECT_2:2

for i, j, k being Nat

for D being non empty set

for f being FinSequence of D st i > j & i in dom f & j in dom f & k in dom (mid (f,i,j)) holds

(i -' k) + 1 in dom f

for D being non empty set

for f being FinSequence of D st i > j & i in dom f & j in dom f & k in dom (mid (f,i,j)) holds

(i -' k) + 1 in dom f

proof end;

theorem Th3: :: SPRECT_2:3

for i, j, k being Nat

for D being non empty set

for f being FinSequence of D st i <= j & i in dom f & j in dom f & k in dom (mid (f,i,j)) holds

(mid (f,i,j)) /. k = f /. ((k + i) -' 1)

for D being non empty set

for f being FinSequence of D st i <= j & i in dom f & j in dom f & k in dom (mid (f,i,j)) holds

(mid (f,i,j)) /. k = f /. ((k + i) -' 1)

proof end;

theorem Th4: :: SPRECT_2:4

for i, j, k being Nat

for D being non empty set

for f being FinSequence of D st i > j & i in dom f & j in dom f & k in dom (mid (f,i,j)) holds

(mid (f,i,j)) /. k = f /. ((i -' k) + 1)

for D being non empty set

for f being FinSequence of D st i > j & i in dom f & j in dom f & k in dom (mid (f,i,j)) holds

(mid (f,i,j)) /. k = f /. ((i -' k) + 1)

proof end;

theorem Th5: :: SPRECT_2:5

for i, j being Nat

for D being non empty set

for f being FinSequence of D st i in dom f & j in dom f holds

len (mid (f,i,j)) >= 1

for D being non empty set

for f being FinSequence of D st i in dom f & j in dom f holds

len (mid (f,i,j)) >= 1

proof end;

theorem Th6: :: SPRECT_2:6

for i, j being Nat

for D being non empty set

for f being FinSequence of D st i in dom f & j in dom f & len (mid (f,i,j)) = 1 holds

i = j

for D being non empty set

for f being FinSequence of D st i in dom f & j in dom f & len (mid (f,i,j)) = 1 holds

i = j

proof end;

theorem Th7: :: SPRECT_2:7

for i, j being Nat

for D being non empty set

for f being FinSequence of D st i in dom f & j in dom f holds

not mid (f,i,j) is empty

for D being non empty set

for f being FinSequence of D st i in dom f & j in dom f holds

not mid (f,i,j) is empty

proof end;

theorem Th8: :: SPRECT_2:8

for i, j being Nat

for D being non empty set

for f being FinSequence of D st i in dom f & j in dom f holds

(mid (f,i,j)) /. 1 = f /. i

for D being non empty set

for f being FinSequence of D st i in dom f & j in dom f holds

(mid (f,i,j)) /. 1 = f /. i

proof end;

theorem Th9: :: SPRECT_2:9

for i, j being Nat

for D being non empty set

for f being FinSequence of D st i in dom f & j in dom f holds

(mid (f,i,j)) /. (len (mid (f,i,j))) = f /. j

for D being non empty set

for f being FinSequence of D st i in dom f & j in dom f holds

(mid (f,i,j)) /. (len (mid (f,i,j))) = f /. j

proof end;

theorem Th10: :: SPRECT_2:10

for X being compact Subset of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in X & p `2 = N-bound X holds

p in N-most X

for p being Point of (TOP-REAL 2) st p in X & p `2 = N-bound X holds

p in N-most X

proof end;

theorem Th11: :: SPRECT_2:11

for X being compact Subset of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in X & p `2 = S-bound X holds

p in S-most X

for p being Point of (TOP-REAL 2) st p in X & p `2 = S-bound X holds

p in S-most X

proof end;

theorem Th12: :: SPRECT_2:12

for X being compact Subset of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in X & p `1 = W-bound X holds

p in W-most X

for p being Point of (TOP-REAL 2) st p in X & p `1 = W-bound X holds

p in W-most X

proof end;

theorem Th13: :: SPRECT_2:13

for X being compact Subset of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st p in X & p `1 = E-bound X holds

p in E-most X

for p being Point of (TOP-REAL 2) st p in X & p `1 = E-bound X holds

p in E-most X

proof end;

theorem Th14: :: SPRECT_2:14

for i, j being Nat

for f being FinSequence of (TOP-REAL 2) st 1 <= i & i <= j & j <= len f holds

L~ (mid (f,i,j)) = union { (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) }

for f being FinSequence of (TOP-REAL 2) st 1 <= i & i <= j & j <= len f holds

L~ (mid (f,i,j)) = union { (LSeg (f,k)) where k is Nat : ( i <= k & k < j ) }

proof end;

theorem Th17: :: SPRECT_2:17

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

( a `1 = b `1 & c `1 = b `1 )

( a `1 = b `1 & c `1 = b `1 )

proof end;

theorem Th18: :: SPRECT_2:18

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

( a `2 = b `2 & c `2 = b `2 )

( a `2 = b `2 & c `2 = b `2 )

proof end;

theorem Th19: :: SPRECT_2:19

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

( a `1 = b `1 & c `1 = b `1 )

( a `1 = b `1 & c `1 = b `1 )

proof end;

theorem Th20: :: SPRECT_2:20

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

( a `2 = b `2 & c `2 = b `2 )

( a `2 = b `2 & c `2 = b `2 )

proof end;

:: deftheorem defines is_in_the_area_of SPRECT_2:def 1 :

for f, g being FinSequence of (TOP-REAL 2) holds

( g is_in_the_area_of f iff for n being Nat st n in dom g holds

( W-bound (L~ f) <= (g /. n) `1 & (g /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (g /. n) `2 & (g /. n) `2 <= N-bound (L~ f) ) );

for f, g being FinSequence of (TOP-REAL 2) holds

( g is_in_the_area_of f iff for n being Nat st n in dom g holds

( W-bound (L~ f) <= (g /. n) `1 & (g /. n) `1 <= E-bound (L~ f) & S-bound (L~ f) <= (g /. n) `2 & (g /. n) `2 <= N-bound (L~ f) ) );

theorem Th22: :: SPRECT_2:22

for f, g being FinSequence of (TOP-REAL 2) st g is_in_the_area_of f holds

for i, j being Nat st i in dom g & j in dom g holds

mid (g,i,j) is_in_the_area_of f

for i, j being Nat st i in dom g & j in dom g holds

mid (g,i,j) is_in_the_area_of f

proof end;

theorem :: SPRECT_2:23

theorem Th24: :: SPRECT_2:24

for f, g, h being FinSequence of (TOP-REAL 2) st g is_in_the_area_of f & h is_in_the_area_of f holds

g ^ h is_in_the_area_of f

g ^ h is_in_the_area_of f

proof end;

theorem Th25: :: SPRECT_2:25

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

proof end;

theorem Th26: :: SPRECT_2:26

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

proof end;

theorem Th27: :: SPRECT_2:27

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

proof end;

theorem Th28: :: SPRECT_2:28

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

proof end;

definition

let f, g be FinSequence of (TOP-REAL 2);

end;
pred g is_a_h.c._for f means :: SPRECT_2:def 2

( g is_in_the_area_of f & (g /. 1) `1 = W-bound (L~ f) & (g /. (len g)) `1 = E-bound (L~ f) );

( g is_in_the_area_of f & (g /. 1) `1 = W-bound (L~ f) & (g /. (len g)) `1 = E-bound (L~ f) );

pred g is_a_v.c._for f means :: SPRECT_2:def 3

( g is_in_the_area_of f & (g /. 1) `2 = S-bound (L~ f) & (g /. (len g)) `2 = N-bound (L~ f) );

( g is_in_the_area_of f & (g /. 1) `2 = S-bound (L~ f) & (g /. (len g)) `2 = N-bound (L~ f) );

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

for f, g being FinSequence of (TOP-REAL 2) holds

( g is_a_h.c._for f iff ( g is_in_the_area_of f & (g /. 1) `1 = W-bound (L~ f) & (g /. (len g)) `1 = E-bound (L~ f) ) );

for f, g being FinSequence of (TOP-REAL 2) holds

( g is_a_h.c._for f iff ( g is_in_the_area_of f & (g /. 1) `1 = W-bound (L~ f) & (g /. (len g)) `1 = E-bound (L~ f) ) );

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

for f, g being FinSequence of (TOP-REAL 2) holds

( g is_a_v.c._for f iff ( g is_in_the_area_of f & (g /. 1) `2 = S-bound (L~ f) & (g /. (len g)) `2 = N-bound (L~ f) ) );

for f, g being FinSequence of (TOP-REAL 2) holds

( g is_a_v.c._for f iff ( g is_in_the_area_of f & (g /. 1) `2 = S-bound (L~ f) & (g /. (len g)) `2 = N-bound (L~ f) ) );

theorem Th29: :: SPRECT_2:29

for f being FinSequence of (TOP-REAL 2)

for g, h being one-to-one special FinSequence of (TOP-REAL 2) st 2 <= len g & 2 <= len h & g is_a_h.c._for f & h is_a_v.c._for f holds

L~ g meets L~ h

for g, h being one-to-one special FinSequence of (TOP-REAL 2) st 2 <= len g & 2 <= len h & g is_a_h.c._for f & h is_a_v.c._for f holds

L~ g meets L~ h

proof end;

definition

let f be FinSequence of (TOP-REAL 2);

end;
attr f is clockwise_oriented means :: SPRECT_2:def 4

(Rotate (f,(N-min (L~ f)))) /. 2 in N-most (L~ f);

(Rotate (f,(N-min (L~ f)))) /. 2 in N-most (L~ f);

:: deftheorem defines clockwise_oriented SPRECT_2:def 4 :

for f being FinSequence of (TOP-REAL 2) holds

( f is clockwise_oriented iff (Rotate (f,(N-min (L~ f)))) /. 2 in N-most (L~ f) );

for f being FinSequence of (TOP-REAL 2) holds

( f is clockwise_oriented iff (Rotate (f,(N-min (L~ f)))) /. 2 in N-most (L~ f) );

theorem Th30: :: SPRECT_2:30

for f being V22() standard special_circular_sequence st f /. 1 = N-min (L~ f) holds

( f is clockwise_oriented iff f /. 2 in N-most (L~ f) ) by FINSEQ_6:89;

( f is clockwise_oriented iff f /. 2 in N-most (L~ f) ) by FINSEQ_6:89;

registration
end;

registration

let X be non empty compact non horizontal non vertical Subset of (TOP-REAL 2);

coherence

SpStSeq X is clockwise_oriented

end;
coherence

SpStSeq X is clockwise_oriented

proof end;

registration

ex b_{1} being V22() standard special_circular_sequence st b_{1} is clockwise_oriented
end;

cluster V1() V4( NAT ) V5( the carrier of (TOP-REAL 2)) non empty non trivial V16() Function-like V22() V28() FinSequence-like FinSubsequence-like circular special unfolded s.c.c. standard clockwise_oriented for FinSequence of the carrier of (TOP-REAL 2);

existence ex b

proof end;

theorem Th37: :: SPRECT_2:37

for f being V22() standard special_circular_sequence

for i, j being Nat st i > j & ( ( 1 < j & i <= len f ) or ( 1 <= j & i < len f ) ) holds

mid (f,i,j) is S-Sequence_in_R2

for i, j being Nat st i > j & ( ( 1 < j & i <= len f ) or ( 1 <= j & i < len f ) ) holds

mid (f,i,j) is S-Sequence_in_R2

proof end;

theorem Th38: :: SPRECT_2:38

for f being V22() standard special_circular_sequence

for i, j being Nat st i < j & ( ( 1 < i & j <= len f ) or ( 1 <= i & j < len f ) ) holds

mid (f,i,j) is S-Sequence_in_R2

for i, j being Nat st i < j & ( ( 1 < i & j <= len f ) or ( 1 <= i & j < len f ) ) holds

mid (f,i,j) is S-Sequence_in_R2

proof end;

theorem Th47: :: SPRECT_2:47

for i, j, m, n being Nat

for f being V22() standard special_circular_sequence st 1 <= i & i <= j & j < m & m <= n & n <= len f & ( 1 < i or n < len f ) holds

L~ (mid (f,i,j)) misses L~ (mid (f,m,n))

for f being V22() standard special_circular_sequence st 1 <= i & i <= j & j < m & m <= n & n <= len f & ( 1 < i or n < len f ) holds

L~ (mid (f,i,j)) misses L~ (mid (f,m,n))

proof end;

theorem Th48: :: SPRECT_2:48

for i, j, m, n being Nat

for f being V22() standard special_circular_sequence st 1 <= i & i <= j & j < m & m <= n & n <= len f & ( 1 < i or n < len f ) holds

L~ (mid (f,i,j)) misses L~ (mid (f,n,m))

for f being V22() standard special_circular_sequence st 1 <= i & i <= j & j < m & m <= n & n <= len f & ( 1 < i or n < len f ) holds

L~ (mid (f,i,j)) misses L~ (mid (f,n,m))

proof end;

theorem Th49: :: SPRECT_2:49

for i, j, m, n being Nat

for f being V22() standard special_circular_sequence st 1 <= i & i <= j & j < m & m <= n & n <= len f & ( 1 < i or n < len f ) holds

L~ (mid (f,j,i)) misses L~ (mid (f,n,m))

for f being V22() standard special_circular_sequence st 1 <= i & i <= j & j < m & m <= n & n <= len f & ( 1 < i or n < len f ) holds

L~ (mid (f,j,i)) misses L~ (mid (f,n,m))

proof end;

theorem Th50: :: SPRECT_2:50

for i, j, m, n being Nat

for f being V22() standard special_circular_sequence st 1 <= i & i <= j & j < m & m <= n & n <= len f & ( 1 < i or n < len f ) holds

L~ (mid (f,j,i)) misses L~ (mid (f,m,n))

for f being V22() standard special_circular_sequence st 1 <= i & i <= j & j < m & m <= n & n <= len f & ( 1 < i or n < len f ) holds

L~ (mid (f,j,i)) misses L~ (mid (f,m,n))

proof end;

theorem Th59: :: SPRECT_2:59

for f being V22() standard special_circular_sequence holds LSeg ((NW-corner (L~ f)),(N-min (L~ f))) misses LSeg ((N-max (L~ f)),(NE-corner (L~ f)))

proof end;

theorem Th60: :: SPRECT_2:60

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st f is being_S-Seq & p <> f /. 1 & ( p `1 = (f /. 1) `1 or p `2 = (f /. 1) `2 ) & (LSeg (p,(f /. 1))) /\ (L~ f) = {(f /. 1)} holds

<*p*> ^ f is S-Sequence_in_R2

for p being Point of (TOP-REAL 2) st f is being_S-Seq & p <> f /. 1 & ( p `1 = (f /. 1) `1 or p `2 = (f /. 1) `2 ) & (LSeg (p,(f /. 1))) /\ (L~ f) = {(f /. 1)} holds

<*p*> ^ f is S-Sequence_in_R2

proof end;

theorem Th61: :: SPRECT_2:61

for f being FinSequence of (TOP-REAL 2)

for p being Point of (TOP-REAL 2) st f is being_S-Seq & p <> f /. (len f) & ( p `1 = (f /. (len f)) `1 or p `2 = (f /. (len f)) `2 ) & (LSeg (p,(f /. (len f)))) /\ (L~ f) = {(f /. (len f))} holds

f ^ <*p*> is S-Sequence_in_R2

for p being Point of (TOP-REAL 2) st f is being_S-Seq & p <> f /. (len f) & ( p `1 = (f /. (len f)) `1 or p `2 = (f /. (len f)) `2 ) & (LSeg (p,(f /. (len f)))) /\ (L~ f) = {(f /. (len f))} holds

f ^ <*p*> is S-Sequence_in_R2

proof end;

theorem Th62: :: SPRECT_2:62

for f being V22() standard special_circular_sequence

for i, j being Nat st i in dom f & j in dom f & mid (f,i,j) is S-Sequence_in_R2 & f /. j = N-max (L~ f) & N-max (L~ f) <> NE-corner (L~ f) holds

(mid (f,i,j)) ^ <*(NE-corner (L~ f))*> is S-Sequence_in_R2

for i, j being Nat st i in dom f & j in dom f & mid (f,i,j) is S-Sequence_in_R2 & f /. j = N-max (L~ f) & N-max (L~ f) <> NE-corner (L~ f) holds

(mid (f,i,j)) ^ <*(NE-corner (L~ f))*> is S-Sequence_in_R2

proof end;

theorem :: SPRECT_2:63

for f being V22() standard special_circular_sequence

for i, j being Nat st i in dom f & j in dom f & mid (f,i,j) is S-Sequence_in_R2 & f /. j = E-max (L~ f) & E-max (L~ f) <> NE-corner (L~ f) holds

(mid (f,i,j)) ^ <*(NE-corner (L~ f))*> is S-Sequence_in_R2

for i, j being Nat st i in dom f & j in dom f & mid (f,i,j) is S-Sequence_in_R2 & f /. j = E-max (L~ f) & E-max (L~ f) <> NE-corner (L~ f) holds

(mid (f,i,j)) ^ <*(NE-corner (L~ f))*> is S-Sequence_in_R2

proof end;

theorem Th64: :: SPRECT_2:64

for f being V22() standard special_circular_sequence

for i, j being Nat st i in dom f & j in dom f & mid (f,i,j) is S-Sequence_in_R2 & f /. j = S-max (L~ f) & S-max (L~ f) <> SE-corner (L~ f) holds

(mid (f,i,j)) ^ <*(SE-corner (L~ f))*> is S-Sequence_in_R2

for i, j being Nat st i in dom f & j in dom f & mid (f,i,j) is S-Sequence_in_R2 & f /. j = S-max (L~ f) & S-max (L~ f) <> SE-corner (L~ f) holds

(mid (f,i,j)) ^ <*(SE-corner (L~ f))*> is S-Sequence_in_R2

proof end;

theorem Th65: :: SPRECT_2:65

for f being V22() standard special_circular_sequence

for i, j being Nat st i in dom f & j in dom f & mid (f,i,j) is S-Sequence_in_R2 & f /. j = E-max (L~ f) & E-max (L~ f) <> NE-corner (L~ f) holds

(mid (f,i,j)) ^ <*(NE-corner (L~ f))*> is S-Sequence_in_R2

for i, j being Nat st i in dom f & j in dom f & mid (f,i,j) is S-Sequence_in_R2 & f /. j = E-max (L~ f) & E-max (L~ f) <> NE-corner (L~ f) holds

(mid (f,i,j)) ^ <*(NE-corner (L~ f))*> is S-Sequence_in_R2

proof end;

theorem Th66: :: SPRECT_2:66

for f being V22() standard special_circular_sequence

for i, j being Nat st i in dom f & j in dom f & mid (f,i,j) is S-Sequence_in_R2 & f /. i = N-min (L~ f) & N-min (L~ f) <> NW-corner (L~ f) holds

<*(NW-corner (L~ f))*> ^ (mid (f,i,j)) is S-Sequence_in_R2

for i, j being Nat st i in dom f & j in dom f & mid (f,i,j) is S-Sequence_in_R2 & f /. i = N-min (L~ f) & N-min (L~ f) <> NW-corner (L~ f) holds

<*(NW-corner (L~ f))*> ^ (mid (f,i,j)) is S-Sequence_in_R2

proof end;

theorem Th67: :: SPRECT_2:67

for f being V22() standard special_circular_sequence

for i, j being Nat st i in dom f & j in dom f & mid (f,i,j) is S-Sequence_in_R2 & f /. i = W-min (L~ f) & W-min (L~ f) <> SW-corner (L~ f) holds

<*(SW-corner (L~ f))*> ^ (mid (f,i,j)) is S-Sequence_in_R2

for i, j being Nat st i in dom f & j in dom f & mid (f,i,j) is S-Sequence_in_R2 & f /. i = W-min (L~ f) & W-min (L~ f) <> SW-corner (L~ f) holds

<*(SW-corner (L~ f))*> ^ (mid (f,i,j)) is S-Sequence_in_R2

proof end;

Lm1: for f being V22() standard special_circular_sequence

for i, j being Nat st i in dom f & j in dom f & mid (f,i,j) is S-Sequence_in_R2 & f /. i = N-min (L~ f) & N-min (L~ f) <> NW-corner (L~ f) & f /. j = N-max (L~ f) & N-max (L~ f) <> NE-corner (L~ f) holds

(<*(NW-corner (L~ f))*> ^ (mid (f,i,j))) ^ <*(NE-corner (L~ f))*> is S-Sequence_in_R2

proof end;

registration

let f be V22() standard special_circular_sequence;

coherence

L~ f is being_simple_closed_curve by JORDAN4:51;

end;
coherence

L~ f is being_simple_closed_curve by JORDAN4:51;

Lm2: for f being V22() standard special_circular_sequence holds LSeg ((S-max (L~ f)),(SE-corner (L~ f))) misses LSeg ((NW-corner (L~ f)),(N-min (L~ f)))

proof end;

Lm3: for f being V22() standard special_circular_sequence

for i, j being Nat st i in dom f & j in dom f & mid (f,i,j) is S-Sequence_in_R2 & f /. i = N-min (L~ f) & N-min (L~ f) <> NW-corner (L~ f) & f /. j = S-max (L~ f) & S-max (L~ f) <> SE-corner (L~ f) holds

(<*(NW-corner (L~ f))*> ^ (mid (f,i,j))) ^ <*(SE-corner (L~ f))*> is S-Sequence_in_R2

proof end;

theorem Th68: :: SPRECT_2:68

for f being V22() standard special_circular_sequence st f /. 1 = N-min (L~ f) holds

(N-min (L~ f)) .. f < (N-max (L~ f)) .. f

(N-min (L~ f)) .. f < (N-max (L~ f)) .. f

proof end;

theorem :: SPRECT_2:69

for f being V22() standard special_circular_sequence st f /. 1 = N-min (L~ f) holds

(N-max (L~ f)) .. f > 1

(N-max (L~ f)) .. f > 1

proof end;

Lm4: for f being V22() standard special_circular_sequence st f /. 1 = N-min (L~ f) holds

(N-min (L~ f)) .. f < (E-max (L~ f)) .. f

proof end;

Lm5: for z being V22() 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;

Lm6: for z being V22() 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 :: SPRECT_2:70

for z being V22() standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) & N-max (L~ z) <> E-max (L~ z) holds

(N-max (L~ z)) .. z < (E-max (L~ z)) .. z

(N-max (L~ z)) .. z < (E-max (L~ z)) .. z

proof end;

Lm7: for z being V22() 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;

Lm8: for f being V22() standard special_circular_sequence holds (LSeg ((N-min (L~ f)),(NW-corner (L~ f)))) /\ (LSeg ((NE-corner (L~ f)),(E-max (L~ f)))) = {}

proof end;

theorem :: SPRECT_2:71

for z being V22() standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) holds

(E-max (L~ z)) .. z < (E-min (L~ z)) .. z

(E-max (L~ z)) .. z < (E-min (L~ z)) .. z

proof end;

theorem Th72: :: SPRECT_2:72

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

(E-min (L~ z)) .. z < (S-max (L~ z)) .. z

(E-min (L~ z)) .. z < (S-max (L~ z)) .. z

proof end;

theorem Th73: :: SPRECT_2:73

for z being V22() standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) holds

(S-max (L~ z)) .. z < (S-min (L~ z)) .. z

(S-max (L~ z)) .. z < (S-min (L~ z)) .. z

proof end;

Lm9: for z being V22() 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;

Lm10: for z being V22() standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) & N-min (L~ z) <> W-max (L~ z) holds

(E-min (L~ z)) .. z < (W-max (L~ z)) .. z

proof end;

Lm11: for z being V22() 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;

theorem :: SPRECT_2:74

for z being V22() standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) & S-min (L~ z) <> W-min (L~ z) holds

(S-min (L~ z)) .. z < (W-min (L~ z)) .. z

(S-min (L~ z)) .. z < (W-min (L~ z)) .. z

proof end;

theorem Th75: :: SPRECT_2:75

for z being V22() standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) & N-min (L~ z) <> W-max (L~ z) holds

(W-min (L~ z)) .. z < (W-max (L~ z)) .. z

(W-min (L~ z)) .. z < (W-max (L~ z)) .. z

proof end;

theorem :: SPRECT_2:76

for z being V22() standard clockwise_oriented special_circular_sequence st z /. 1 = N-min (L~ z) holds

(W-min (L~ z)) .. z < len z

(W-min (L~ z)) .. z < len z

proof end;

theorem :: SPRECT_2:77

for f being V22() standard special_circular_sequence st f /. 1 = N-min (L~ f) holds

(W-max (L~ f)) .. f < len f

(W-max (L~ f)) .. f < len f

proof end;