:: SPRECT_5 semantic presentation

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
let D be non empty set ; ::_thesis: 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
let f be FinSequence of D; ::_thesis: for q, p being Element of D st q in rng (f | (p .. f)) holds
q .. f <= p .. f
let q, p be Element of D; ::_thesis: ( q in rng (f | (p .. f)) implies q .. f <= p .. f )
assume A1: q in rng (f | (p .. f)) ; ::_thesis: q .. f <= p .. f
then  q .. (f | (p .. f)) = q .. f by FINSEQ_5:40;
then A2: q .. f <= len (f | (p .. f)) by A1, FINSEQ_4:21;
 len (f | (p .. f)) <= p .. f by FINSEQ_5:17;
hence  q .. f <= p .. f by A2, XXREAL_0:2; ::_thesis: verum
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
let D be non empty set ; ::_thesis: 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
let f be FinSequence of D; ::_thesis: 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
let p, q be Element of D; ::_thesis: ( p in rng f & q in rng f & p .. f <= q .. f implies q .. (f :- p) = ((q .. f) - (p .. f)) + 1 )
assume that
A1: p in rng f and
A2: q in rng f and
A3: p .. f <= q .. f ; ::_thesis: q .. (f :- p) = ((q .. f) - (p .. f)) + 1
A4: f = (f | (p .. f)) ^ (f /^ (p .. f)) by RFINSEQ:8;
percases ( p .. f = q .. f or p .. f < q .. f ) by A3, XXREAL_0:1;
suppose p .. f = q .. f ; ::_thesis: q .. (f :- p) = ((q .. f) - (p .. f)) + 1
then  p = q by A1, A2, FINSEQ_5:9;
hence  q .. (f :- p) = ((q .. f) - (p .. f)) + 1 by FINSEQ_6:79; ::_thesis: verum
end;
supposeA5: p .. f < q .. f ; ::_thesis: q .. (f :- p) = ((q .. f) - (p .. f)) + 1
 p .. f <= len f by A1, FINSEQ_4:21;
then A6: len (f | (p .. f)) = p .. f by FINSEQ_1:59;
A7: not q in rng (f | (p .. f)) by A5, Th1;
 q in (rng (f | (p .. f))) \/ (rng (f /^ (p .. f))) by A2, A4, FINSEQ_1:31;
then A8: q in rng (f /^ (p .. f)) by A7, XBOOLE_0:def_3;
then  q in (rng (f /^ (p .. f))) \ (rng (f | (p .. f))) by A7, XBOOLE_0:def_5;
then A9: q .. f = (p .. f) + (q .. (f /^ (p .. f))) by A4, A6, FINSEQ_6:7;
 not q in {p} by A5, TARSKI:def_1;
then  not q in rng <*p*> by FINSEQ_1:38;
then A10: q in (rng (f /^ (p .. f))) \ (rng <*p*>) by A8, XBOOLE_0:def_5;
 f :- p = <*p*> ^ (f /^ (p .. f)) by FINSEQ_5:def_2;
hence q .. (f :- p) = (len <*p*>) + (q .. (f /^ (p .. f))) by A10, FINSEQ_6:7
.= ((q .. f) - (p .. f)) + 1 by A9, FINSEQ_1:39 ;
::_thesis: verum
end;
end;
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
let D be non empty set ; ::_thesis: 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
let f be FinSequence of D; ::_thesis: 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
let p, q be Element of D; ::_thesis: ( p in rng f & q in rng f & p .. f <= q .. f implies p .. (f -: q) = p .. f )
A1: f -: q = f | (q .. f) by FINSEQ_5:def_1;
assume  ( p in rng f & q in rng f & p .. f <= q .. f ) ; ::_thesis: p .. (f -: q) = p .. f
then  p in rng (f | (q .. f)) by A1, FINSEQ_5:46;
hence  p .. (f -: q) = p .. f by A1, FINSEQ_5:40; ::_thesis: verum
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
let D be non empty set ; ::_thesis: 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
let f be FinSequence of D; ::_thesis: 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
let p, q be Element of D; ::_thesis: ( p in rng f & q in rng f & p .. f <= q .. f implies q .. (Rotate (f,p)) = ((q .. f) - (p .. f)) + 1 )
assume that
A1: p in rng f and
A2: q in rng f ; ::_thesis: ( not p .. f <= q .. f or q .. (Rotate (f,p)) = ((q .. f) - (p .. f)) + 1 )
A3: Rotate (f,p) = (f :- p) ^ ((f -: p) /^ 1) by A1, FINSEQ_6:def_2;
assume A4: p .. f <= q .. f ; ::_thesis: q .. (Rotate (f,p)) = ((q .. f) - (p .. f)) + 1
then  q in rng (f :- p) by A1, A2, FINSEQ_6:62;
hence q .. (Rotate (f,p)) = q .. (f :- p) by A3, FINSEQ_6:6
.= ((q .. f) - (p .. f)) + 1 by A1, A2, A4, Th2 ;
::_thesis: verum
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
let D be non empty set ; ::_thesis: 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))
let f be FinSequence of D; ::_thesis: 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))
let p1, p2, p3 be Element of D; ::_thesis: ( p1 in rng f & p2 in rng f & p3 in rng f & p1 .. f <= p2 .. f & p2 .. f < p3 .. f implies p2 .. (Rotate (f,p1)) < p3 .. (Rotate (f,p1)) )
assume that
A1: ( p1 in rng f & p2 in rng f & p3 in rng f & p1 .. f <= p2 .. f ) and
A2: p2 .. f < p3 .. f ; ::_thesis: p2 .. (Rotate (f,p1)) < p3 .. (Rotate (f,p1))
A3: (p2 .. f) - (p1 .. f) < (p3 .. f) - (p1 .. f) by A2, XREAL_1:9;
 ( p2 .. (Rotate (f,p1)) = ((p2 .. f) - (p1 .. f)) + 1 & p3 .. (Rotate (f,p1)) = ((p3 .. f) - (p1 .. f)) + 1 ) by A1, A2, Th4, XXREAL_0:2;
hence  p2 .. (Rotate (f,p1)) < p3 .. (Rotate (f,p1)) by A3, XREAL_1:6; ::_thesis: verum
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
let D be non empty set ; ::_thesis: 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))
let f be FinSequence of D; ::_thesis: 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))
let p1, p2, p3 be Element of D; ::_thesis: ( p1 in rng f & p2 in rng f & p3 in rng f & p1 .. f < p2 .. f & p2 .. f <= p3 .. f implies p2 .. (Rotate (f,p1)) <= p3 .. (Rotate (f,p1)) )
assume that
A1: p1 in rng f and
A2: ( p2 in rng f & p3 in rng f ) and
A3: p1 .. f < p2 .. f and
A4: p2 .. f <= p3 .. f ; ::_thesis: p2 .. (Rotate (f,p1)) <= p3 .. (Rotate (f,p1))
percases ( p2 .. f < p3 .. f or p2 .. f = p3 .. f ) by A4, XXREAL_0:1;
suppose p2 .. f < p3 .. f ; ::_thesis: p2 .. (Rotate (f,p1)) <= p3 .. (Rotate (f,p1))
hence  p2 .. (Rotate (f,p1)) <= p3 .. (Rotate (f,p1)) by A1, A2, A3, Th5; ::_thesis: verum
end;
suppose p2 .. f = p3 .. f ; ::_thesis: p2 .. (Rotate (f,p1)) <= p3 .. (Rotate (f,p1))
hence  p2 .. (Rotate (f,p1)) <= p3 .. (Rotate (f,p1)) by A2, FINSEQ_5:9; ::_thesis: verum
end;
end;
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
let D be non empty set ; ::_thesis: 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
let g be circular FinSequence of D; ::_thesis: for p being Element of D st p in rng g & len g > 1 holds
p .. g < len g
let p be Element of D; ::_thesis: ( p in rng g & len g > 1 implies p .. g < len g )
assume that
A1: p in rng g and
A2: len g > 1 and
A3: p .. g >= len g ; ::_thesis: contradiction
 p .. g <= len g by A1, FINSEQ_4:21;
then  p .. g = len g by A3, XXREAL_0:1;
then A4: p = g /. (len g) by A1, FINSEQ_5:38
.= g /. 1 by FINSEQ_6:def_1 ;
 not g is empty by A2, CARD_1:27;
hence  contradiction by A2, A3, A4, FINSEQ_6:43; ::_thesis: verum
end;

begin


registration
let f be non constant standard special_circular_sequence;
clusterf /^ 1 ->  one-to-one ;
coherence
 f /^ 1 is one-to-one
proof
let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in K49((f /^ 1)) or not x2 in K49((f /^ 1)) or not (f /^ 1) . x1 = (f /^ 1) . x2 or x1 = x2 )
assume that
A1: x1 in dom (f /^ 1) and
A2: x2 in dom (f /^ 1) and
A3: (f /^ 1) . x1 = (f /^ 1) . x2 ; ::_thesis: x1 = x2
reconsider i = x1, j = x2 as Element of NAT by A1, A2;
 1 <= i by A1, FINSEQ_3:25;
then A4: 1 < i + 1 by NAT_1:13;
 i + 1 in dom f by A1, FINSEQ_5:26;
then A5: i + 1 <= len f by FINSEQ_3:25;
 1 <= j by A2, FINSEQ_3:25;
then A6: 1 < j + 1 by NAT_1:13;
 j + 1 in dom f by A2, FINSEQ_5:26;
then A7: j + 1 <= len f by FINSEQ_3:25;
assume A8: x1 <> x2 ; ::_thesis: contradiction
percases ( i < j or j < i ) by A8, XXREAL_0:1;
suppose i < j ; ::_thesis: contradiction
then A9: i + 1 < j + 1 by XREAL_1:6;
f /. (i + 1) = (f /^ 1) /. i by A1, FINSEQ_5:27
.= (f /^ 1) . j by A1, A3, PARTFUN1:def_6
.= (f /^ 1) /. j by A2, PARTFUN1:def_6
.= f /. (j + 1) by A2, FINSEQ_5:27 ;
hence  contradiction by A4, A7, A9, GOBOARD7:37; ::_thesis: verum
end;
suppose j < i ; ::_thesis: contradiction
then A10: j + 1 < i + 1 by XREAL_1:6;
f /. (j + 1) = (f /^ 1) /. j by A2, FINSEQ_5:27
.= (f /^ 1) . i by A2, A3, PARTFUN1:def_6
.= (f /^ 1) /. i by A1, PARTFUN1:def_6
.= f /. (i + 1) by A1, FINSEQ_5:27 ;
hence  contradiction by A5, A6, A10, GOBOARD7:37; ::_thesis: verum
end;
end;
end;
end;

theorem Th8: :: SPRECT_5:8
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
let f be non constant standard special_circular_sequence; ::_thesis: 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)
let q be Point of (TOP-REAL 2); ::_thesis: ( 1 < q .. f & q in rng f implies (f /. 1) .. (Rotate (f,q)) = ((len f) + 1) - (q .. f) )
assume that
A1: 1 < q .. f and
A2: q in rng f ; ::_thesis: (f /. 1) .. (Rotate (f,q)) = ((len f) + 1) - (q .. f)
set i = (1 + (len f)) -' (q .. f);
A3: (q .. f) - 1 > 0 by A1, XREAL_1:50;
A4: q .. f <= len f by A2, FINSEQ_4:21;
then A5: q .. f <= (len f) + 1 by NAT_1:13;
then A6: (1 + (len f)) -' (q .. f) = (1 + (len f)) - (q .. f) by XREAL_1:233;
then  ((1 + (len f)) -' (q .. f)) + ((q .. f) - 1) = len f ;
then  (1 + (len f)) -' (q .. f) < len f by A3, XREAL_1:29;
then A7: (1 + (len f)) -' (q .. f) < len (Rotate (f,q)) by REVROT_1:14;
now__::_thesis:_not_(q_.._f)_+_0_>=_len_f
assume  (q .. f) + 0 >= len f ; ::_thesis: contradiction
then A8: q .. f = len f by A4, XXREAL_0:1;
q = f /. (q .. f) by A2, FINSEQ_5:38
.= f /. 1 by A8, FINSEQ_6:def_1 ;
hence  contradiction by A1, FINSEQ_6:43; ::_thesis: verum
end;
then A9: (len f) - (q .. f) > 0 by XREAL_1:20;
 (1 + (len f)) -' (q .. f) = 1 + ((len f) - (q .. f)) by A6;
then A10: 1 + 0 < (1 + (len f)) -' (q .. f) by A9, XREAL_1:6;
then A11: (1 + (len f)) -' (q .. f) in dom (Rotate (f,q)) by A7, FINSEQ_3:25;
A12: f /. 1 = (Rotate (f,q)) /. ((1 + (len f)) -' (q .. f)) by A1, A2, REVROT_1:18;
then A13: f /. 1 = (Rotate (f,q)) . ((1 + (len f)) -' (q .. f)) by A11, PARTFUN1:def_6;
 for j being set st j in dom (Rotate (f,q)) & j <> (1 + (len f)) -' (q .. f) holds
(Rotate (f,q)) . j <> f /. 1
proof
let z be set ; ::_thesis: ( z in dom (Rotate (f,q)) & z <> (1 + (len f)) -' (q .. f) implies (Rotate (f,q)) . z <> f /. 1 )
assume that
A14: z in dom (Rotate (f,q)) and
A15: z <> (1 + (len f)) -' (q .. f) ; ::_thesis: (Rotate (f,q)) . z <> f /. 1
reconsider j = z as Element of NAT by A14;
percases ( j < (1 + (len f)) -' (q .. f) or (1 + (len f)) -' (q .. f) < j ) by A15, XXREAL_0:1;
supposeA16: j < (1 + (len f)) -' (q .. f) ; ::_thesis: (Rotate (f,q)) . z <> f /. 1
 1 <= j by A14, FINSEQ_3:25;
then  (Rotate (f,q)) /. j <> f /. 1 by A12, A7, A16, GOBOARD7:36;
hence  (Rotate (f,q)) . z <> f /. 1 by A14, PARTFUN1:def_6; ::_thesis: verum
end;
supposeA17: (1 + (len f)) -' (q .. f) < j ; ::_thesis: (Rotate (f,q)) . z <> f /. 1
 j <= len (Rotate (f,q)) by A14, FINSEQ_3:25;
then  (Rotate (f,q)) /. j <> f /. 1 by A12, A10, A17, GOBOARD7:37;
hence  (Rotate (f,q)) . z <> f /. 1 by A14, PARTFUN1:def_6; ::_thesis: verum
end;
end;
end;
then A18: Rotate (f,q) just_once_values f /. 1 by A11, A13, FINSEQ_4:7;
then  (1 + (len f)) -' (q .. f) = (Rotate (f,q)) <- (f /. 1) by A11, A13, FINSEQ_4:def_3;
hence (f /. 1) .. (Rotate (f,q)) = (1 + (len f)) -' (q .. f) by A18, FINSEQ_4:25
.= ((len f) + 1) - (q .. f) by A5, XREAL_1:233 ;
::_thesis: verum
end;

theorem Th9: :: SPRECT_5:9
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
let f be non constant standard special_circular_sequence; ::_thesis: 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)
let p, q be Point of (TOP-REAL 2); ::_thesis: ( p in rng f & q in rng f & p .. f < q .. f implies p .. (Rotate (f,q)) = ((len f) + (p .. f)) - (q .. f) )
assume that
A1: p in rng f and
A2: q in rng f ; ::_thesis: ( not p .. f < q .. f or p .. (Rotate (f,q)) = ((len f) + (p .. f)) - (q .. f) )
assume A3: p .. f < q .. f ; ::_thesis: p .. (Rotate (f,q)) = ((len f) + (p .. f)) - (q .. f)
then A4: p .. f = p .. (f -: q) by A1, A2, Th3;
A5: p in rng (f -: q) by A1, A2, A3, FINSEQ_5:46;
then A6: p .. (f -: q) >= 1 by FINSEQ_4:21;
A7: Rotate (f,q) = (f :- q) ^ ((f -: q) /^ 1) by A2, FINSEQ_6:def_2;
percases ( p .. f = 1 or p .. f > 1 ) by A6, A4, XXREAL_0:1;
supposeA8: p .. f = 1 ; ::_thesis: p .. (Rotate (f,q)) = ((len f) + (p .. f)) - (q .. f)
then  p = f /. 1 by A1, FINSEQ_5:38;
hence  p .. (Rotate (f,q)) = ((len f) + (p .. f)) - (q .. f) by A2, A3, A8, Th8; ::_thesis: verum
end;
supposeA9: p .. f > 1 ; ::_thesis: p .. (Rotate (f,q)) = ((len f) + (p .. f)) - (q .. f)
then A10: p .. f = 1 + (p .. ((f -: q) /^ 1)) by A5, A4, FINSEQ_6:56;
 not p in {q} by A3, TARSKI:def_1;
then A11: not p in rng <*q*> by FINSEQ_1:38;
A12: q in rng (f /^ 1) by A2, A3, A9, FINSEQ_6:78;
then ((f /^ 1) -| q) ^ <*q*> = (f /^ 1) | (q .. (f /^ 1)) by FINSEQ_5:24
.= (f /^ 1) -: q by FINSEQ_5:def_1 ;
then A13: rng ((f /^ 1) -: q) = (rng ((f /^ 1) -| q)) \/ (rng <*q*>) by FINSEQ_1:31;
A14: rng ((f /^ 1) -| q) misses rng ((f /^ 1) |-- q) by A12, FINSEQ_4:57;
 (f /^ 1) :- q = <*q*> ^ ((f /^ 1) |-- q) by A12, FINSEQ_6:41;
then A15: rng ((f /^ 1) :- q) = (rng <*q*>) \/ (rng ((f /^ 1) |-- q)) by FINSEQ_1:31;
 p .. (f -: q) > 1 by A1, A2, A3, A9, Th3;
then A16: p in rng ((f -: q) /^ 1) by A5, FINSEQ_6:57;
then  p in rng ((f /^ 1) -: q) by A2, A3, A9, FINSEQ_6:60;
then  p in rng ((f /^ 1) -| q) by A13, A11, XBOOLE_0:def_3;
then  not p in rng ((f /^ 1) |-- q) by A14, XBOOLE_0:3;
then  not p in rng ((f /^ 1) :- q) by A11, A15, XBOOLE_0:def_3;
then  not p in rng (f :- q) by A2, A3, A9, FINSEQ_6:83;
then  p in (rng ((f -: q) /^ 1)) \ (rng (f :- q)) by A16, XBOOLE_0:def_5;
hence p .. (Rotate (f,q)) = (len (f :- q)) + (p .. ((f -: q) /^ 1)) by A7, FINSEQ_6:7
.= (((len f) - (q .. f)) + 1) + ((p .. f) - 1) by A2, A10, FINSEQ_5:50
.= ((len f) + (p .. f)) - (q .. f) ;
::_thesis: verum
end;
end;
end;

theorem Th10: :: SPRECT_5:10
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
let f be non constant standard special_circular_sequence; ::_thesis: 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))
let p1, p2, p3 be Point of (TOP-REAL 2); ::_thesis: ( p1 in rng f & p2 in rng f & p3 in rng f & p1 .. f < p2 .. f & p2 .. f < p3 .. f implies p3 .. (Rotate (f,p2)) < p1 .. (Rotate (f,p2)) )
assume that
A1: p1 in rng f and
A2: p2 in rng f and
A3: p3 in rng f and
A4: p1 .. f < p2 .. f and
A5: p2 .. f < p3 .. f ; ::_thesis: p3 .. (Rotate (f,p2)) < p1 .. (Rotate (f,p2))
A6: ( p1 in rng (Rotate (f,p2)) & p3 in rng (Rotate (f,p2)) ) by A1, A2, A3, FINSEQ_6:90;
 ( 1 <= p1 .. f & p3 .. f <= len f ) by A1, A3, FINSEQ_4:21;
then A7: (p3 .. f) + 1 <= (len f) + (p1 .. f) by XREAL_1:7;
A8: p3 .. (Rotate (f,p2)) = ((p3 .. f) - (p2 .. f)) + 1 by A2, A3, A5, Th4
.= ((p3 .. f) + 1) - (p2 .. f) ;
 p1 .. (Rotate (f,p2)) = ((len f) + (p1 .. f)) - (p2 .. f) by A1, A2, A4, Th9;
then  p3 .. (Rotate (f,p2)) <= p1 .. (Rotate (f,p2)) by A8, A7, XREAL_1:9;
hence  p3 .. (Rotate (f,p2)) < p1 .. (Rotate (f,p2)) by A4, A5, A6, FINSEQ_5:9, XXREAL_0:1; ::_thesis: verum
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
p1 .. (Rotate (f,p3)) < p2 .. (Rotate (f,p3))
proof
let f be non constant standard special_circular_sequence; ::_thesis: 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))
let p1, p2, p3 be Point of (TOP-REAL 2); ::_thesis: ( p1 in rng f & p2 in rng f & p3 in rng f & p1 .. f < p2 .. f & p2 .. f < p3 .. f implies p1 .. (Rotate (f,p3)) < p2 .. (Rotate (f,p3)) )
assume that
A1: p1 in rng f and
A2: p2 in rng f and
A3: p3 in rng f and
A4: ( p1 .. f < p2 .. f & p2 .. f < p3 .. f ) ; ::_thesis: p1 .. (Rotate (f,p3)) < p2 .. (Rotate (f,p3))
 p1 .. f < p3 .. f by A4, XXREAL_0:2;
then A5: p1 .. (Rotate (f,p3)) = ((len f) + (p1 .. f)) - (p3 .. f) by A1, A3, Th9;
 ( p2 .. (Rotate (f,p3)) = ((len f) + (p2 .. f)) - (p3 .. f) & (len f) + (p1 .. f) < (len f) + (p2 .. f) ) by A2, A3, A4, Th9, XREAL_1:6;
hence  p1 .. (Rotate (f,p3)) < p2 .. (Rotate (f,p3)) by A5, XREAL_1:9; ::_thesis: verum
end;

theorem :: 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
let f be non constant standard special_circular_sequence; ::_thesis: 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))
let p1, p2, p3 be Point of (TOP-REAL 2); ::_thesis: ( p1 in rng f & p2 in rng f & p3 in rng f & p1 .. f <= p2 .. f & p2 .. f < p3 .. f implies p1 .. (Rotate (f,p3)) <= p2 .. (Rotate (f,p3)) )
assume that
A1: ( p1 in rng f & p2 in rng f ) and
A2: p3 in rng f and
A3: p1 .. f <= p2 .. f and
A4: p2 .. f < p3 .. f ; ::_thesis: p1 .. (Rotate (f,p3)) <= p2 .. (Rotate (f,p3))
percases ( p1 .. f < p2 .. f or p1 .. f = p2 .. f ) by A3, XXREAL_0:1;
suppose p1 .. f < p2 .. f ; ::_thesis: p1 .. (Rotate (f,p3)) <= p2 .. (Rotate (f,p3))
hence  p1 .. (Rotate (f,p3)) <= p2 .. (Rotate (f,p3)) by A1, A2, A4, Th11; ::_thesis: verum
end;
suppose p1 .. f = p2 .. f ; ::_thesis: p1 .. (Rotate (f,p3)) <= p2 .. (Rotate (f,p3))
hence  p1 .. (Rotate (f,p3)) <= p2 .. (Rotate (f,p3)) by A1, FINSEQ_5:9; ::_thesis: verum
end;
end;
end;

theorem :: SPRECT_5:13
for f being non constant standard special_circular_sequence holds (S-min (L~ f)) .. f < len f
proof
let f be non constant standard special_circular_sequence; ::_thesis: (S-min (L~ f)) .. f < len f
 ( S-min (L~ f) in rng f & len f > 1 ) by GOBOARD7:34, SPRECT_2:41, XXREAL_0:2;
hence  (S-min (L~ f)) .. f < len f by Th7; ::_thesis: verum
end;

theorem :: SPRECT_5:14
for f being non constant standard special_circular_sequence holds (S-max (L~ f)) .. f < len f
proof
let f be non constant standard special_circular_sequence; ::_thesis: (S-max (L~ f)) .. f < len f
 ( S-max (L~ f) in rng f & len f > 1 ) by GOBOARD7:34, SPRECT_2:42, XXREAL_0:2;
hence  (S-max (L~ f)) .. f < len f by Th7; ::_thesis: verum
end;

theorem :: SPRECT_5:15
for f being non constant standard special_circular_sequence holds (E-min (L~ f)) .. f < len f
proof
let f be non constant standard special_circular_sequence; ::_thesis: (E-min (L~ f)) .. f < len f
 ( E-min (L~ f) in rng f & len f > 1 ) by GOBOARD7:34, SPRECT_2:45, XXREAL_0:2;
hence  (E-min (L~ f)) .. f < len f by Th7; ::_thesis: verum
end;

theorem :: SPRECT_5:16
for f being non constant standard special_circular_sequence holds (E-max (L~ f)) .. f < len f
proof
let f be non constant standard special_circular_sequence; ::_thesis: (E-max (L~ f)) .. f < len f
 ( E-max (L~ f) in rng f & len f > 1 ) by GOBOARD7:34, SPRECT_2:46, XXREAL_0:2;
hence  (E-max (L~ f)) .. f < len f by Th7; ::_thesis: verum
end;

theorem :: SPRECT_5:17
for f being non constant standard special_circular_sequence holds (N-min (L~ f)) .. f < len f
proof
let f be non constant standard special_circular_sequence; ::_thesis: (N-min (L~ f)) .. f < len f
 ( N-min (L~ f) in rng f & len f > 1 ) by GOBOARD7:34, SPRECT_2:39, XXREAL_0:2;
hence  (N-min (L~ f)) .. f < len f by Th7; ::_thesis: verum
end;

theorem :: SPRECT_5:18
for f being non constant standard special_circular_sequence holds (N-max (L~ f)) .. f < len f
proof
let f be non constant standard special_circular_sequence; ::_thesis: (N-max (L~ f)) .. f < len f
 ( N-max (L~ f) in rng f & len f > 1 ) by GOBOARD7:34, SPRECT_2:40, XXREAL_0:2;
hence  (N-max (L~ f)) .. f < len f by Th7; ::_thesis: verum
end;

theorem :: SPRECT_5:19
for f being non constant standard special_circular_sequence holds (W-max (L~ f)) .. f < len f
proof
let f be non constant standard special_circular_sequence; ::_thesis: (W-max (L~ f)) .. f < len f
 ( W-max (L~ f) in rng f & len f > 1 ) by GOBOARD7:34, SPRECT_2:44, XXREAL_0:2;
hence  (W-max (L~ f)) .. f < len f by Th7; ::_thesis: verum
end;

theorem :: SPRECT_5:20
for f being non constant standard special_circular_sequence holds (W-min (L~ f)) .. f < len f
proof
let f be non constant standard special_circular_sequence; ::_thesis: (W-min (L~ f)) .. f < len f
 ( W-min (L~ f) in rng f & len f > 1 ) by GOBOARD7:34, SPRECT_2:43, XXREAL_0:2;
hence  (W-min (L~ f)) .. f < len f by Th7; ::_thesis: verum
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = N-min (L~ z) implies (E-max (L~ z)) .. z < (S-max (L~ z)) .. z )
assume A1: z /. 1 = N-min (L~ z) ; ::_thesis: (E-max (L~ z)) .. z < (S-max (L~ z)) .. z
then  (E-max (L~ z)) .. z < (E-min (L~ z)) .. z by SPRECT_2:71;
hence  (E-max (L~ z)) .. z < (S-max (L~ z)) .. z by A1, SPRECT_2:72, XXREAL_0:2; ::_thesis: verum
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = N-min (L~ z) implies (E-max (L~ z)) .. z < (S-min (L~ z)) .. z )
assume A1: z /. 1 = N-min (L~ z) ; ::_thesis: (E-max (L~ z)) .. z < (S-min (L~ z)) .. z
then  (E-max (L~ z)) .. z < (S-max (L~ z)) .. z by Lm1;
hence  (E-max (L~ z)) .. z < (S-min (L~ z)) .. z by A1, SPRECT_2:73, XXREAL_0:2; ::_thesis: verum
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = N-min (L~ z) implies (E-max (L~ z)) .. z < (W-min (L~ z)) .. z )
assume A1: z /. 1 = N-min (L~ z) ; ::_thesis: (E-max (L~ z)) .. z < (W-min (L~ z)) .. z
then  (E-max (L~ z)) .. z < (S-min (L~ z)) .. z by Lm2;
hence  (E-max (L~ z)) .. z < (W-min (L~ z)) .. z by A1, SPRECT_2:74, XXREAL_0:2; ::_thesis: verum
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = N-min (L~ z) implies (E-min (L~ z)) .. z < (S-min (L~ z)) .. z )
assume A1: z /. 1 = N-min (L~ z) ; ::_thesis: (E-min (L~ z)) .. z < (S-min (L~ z)) .. z
then  (S-max (L~ z)) .. z < (S-min (L~ z)) .. z by SPRECT_2:73;
hence  (E-min (L~ z)) .. z < (S-min (L~ z)) .. z by A1, SPRECT_2:72, XXREAL_0:2; ::_thesis: verum
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = N-min (L~ z) implies (E-min (L~ z)) .. z < (W-min (L~ z)) .. z )
assume A1: z /. 1 = N-min (L~ z) ; ::_thesis: (E-min (L~ z)) .. z < (W-min (L~ z)) .. z
then  (E-min (L~ z)) .. z < (S-min (L~ z)) .. z by Lm4;
hence  (E-min (L~ z)) .. z < (W-min (L~ z)) .. z by A1, SPRECT_2:74, XXREAL_0:2; ::_thesis: verum
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = N-min (L~ z) implies (S-max (L~ z)) .. z < (W-min (L~ z)) .. z )
assume A1: z /. 1 = N-min (L~ z) ; ::_thesis: (S-max (L~ z)) .. z < (W-min (L~ z)) .. z
then  (S-max (L~ z)) .. z < (S-min (L~ z)) .. z by SPRECT_2:73;
hence  (S-max (L~ z)) .. z < (W-min (L~ z)) .. z by A1, SPRECT_2:74, XXREAL_0:2; ::_thesis: verum
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = N-min (L~ z) implies (N-max (L~ z)) .. z < (W-min (L~ z)) .. z )
assume A1: z /. 1 = N-min (L~ z) ; ::_thesis: (N-max (L~ z)) .. z < (W-min (L~ z)) .. z
then  (E-max (L~ z)) .. z < (W-min (L~ z)) .. z by Lm3;
hence  (N-max (L~ z)) .. z < (W-min (L~ z)) .. z by A1, SPRECT_2:70, XXREAL_0:2; ::_thesis: verum
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = N-min (L~ z) implies (N-min (L~ z)) .. z < (W-min (L~ z)) .. z )
assume A1: z /. 1 = N-min (L~ z) ; ::_thesis: (N-min (L~ z)) .. z < (W-min (L~ z)) .. z
then  (N-max (L~ z)) .. z < (W-min (L~ z)) .. z by Lm7;
hence  (N-min (L~ z)) .. z < (W-min (L~ z)) .. z by A1, SPRECT_2:68, XXREAL_0:2; ::_thesis: verum
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = N-min (L~ z) implies (N-max (L~ z)) .. z < (S-max (L~ z)) .. z )
assume A1: z /. 1 = N-min (L~ z) ; ::_thesis: (N-max (L~ z)) .. z < (S-max (L~ z)) .. z
then  (N-max (L~ z)) .. z <= (E-max (L~ z)) .. z by SPRECT_2:70;
hence  (N-max (L~ z)) .. z < (S-max (L~ z)) .. z by A1, Lm1, XXREAL_0:2; ::_thesis: verum
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = N-min (L~ z) implies (N-max (L~ z)) .. z < (S-min (L~ z)) .. z )
assume A1: z /. 1 = N-min (L~ z) ; ::_thesis: (N-max (L~ z)) .. z < (S-min (L~ z)) .. z
then  (N-max (L~ z)) .. z < (S-max (L~ z)) .. z by Lm9;
hence  (N-max (L~ z)) .. z < (S-min (L~ z)) .. z by A1, SPRECT_2:73, XXREAL_0:2; ::_thesis: verum
end;

theorem Th21: :: SPRECT_5:21
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
let f be non constant standard special_circular_sequence; ::_thesis: ( f /. 1 = W-min (L~ f) implies (W-min (L~ f)) .. f < (W-max (L~ f)) .. f )
assume  f /. 1 = W-min (L~ f) ; ::_thesis: (W-min (L~ f)) .. f < (W-max (L~ f)) .. f
then A1: (W-min (L~ f)) .. f = 1 by FINSEQ_6:43;
A2: W-max (L~ f) in rng f by SPRECT_2:44;
then  (W-max (L~ f)) .. f in dom f by FINSEQ_4:20;
then A3: (W-max (L~ f)) .. f >= 1 by FINSEQ_3:25;
 W-min (L~ f) in rng f by SPRECT_2:43;
then  (W-min (L~ f)) .. f <> (W-max (L~ f)) .. f by A2, FINSEQ_5:9, SPRECT_2:58;
hence  (W-min (L~ f)) .. f < (W-max (L~ f)) .. f by A3, A1, XXREAL_0:1; ::_thesis: verum
end;

theorem :: SPRECT_5:22
for f being non constant standard special_circular_sequence st f /. 1 = W-min (L~ f) holds
(W-max (L~ f)) .. f > 1
proof
let f be non constant standard special_circular_sequence; ::_thesis: ( f /. 1 = W-min (L~ f) implies (W-max (L~ f)) .. f > 1 )
assume A1: f /. 1 = W-min (L~ f) ; ::_thesis: (W-max (L~ f)) .. f > 1
then  (W-min (L~ f)) .. f = 1 by FINSEQ_6:43;
hence  (W-max (L~ f)) .. f > 1 by A1, Th21; ::_thesis: verum
end;

theorem Th23: :: SPRECT_5:23
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = W-min (L~ z) & W-max (L~ z) <> N-min (L~ z) implies (W-max (L~ z)) .. z < (N-min (L~ z)) .. z )
set g = Rotate (z,(N-min (L~ z)));
A1: L~ z = L~ (Rotate (z,(N-min (L~ z)))) by REVROT_1:33;
 N-min (L~ z) in rng z by SPRECT_2:39;
then A2: (Rotate (z,(N-min (L~ z)))) /. 1 = N-min (L~ (Rotate (z,(N-min (L~ z))))) by A1, FINSEQ_6:92;
then A3: (W-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) > (N-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) by Lm8;
assume that
A4: z /. 1 = W-min (L~ z) and
A5: W-max (L~ z) <> N-min (L~ z) ; ::_thesis: (W-max (L~ z)) .. z < (N-min (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A6: Rotate ((Rotate (z,(N-min (L~ z)))),(W-min (L~ z))) = z by A4, REVROT_1:16;
A7: ( N-min (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) & W-max (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) ) by SPRECT_2:39, SPRECT_2:44;
 ( W-min (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) & (W-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) < (W-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) ) by A1, A5, A2, SPRECT_2:43, SPRECT_2:75;
hence  (W-max (L~ z)) .. z < (N-min (L~ z)) .. z by A1, A6, A7, A3, Th10; ::_thesis: verum
end;

theorem Th24: :: SPRECT_5:24
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = W-min (L~ z) implies (N-min (L~ z)) .. z < (N-max (L~ z)) .. z )
set g = Rotate (z,(N-min (L~ z)));
A1: L~ z = L~ (Rotate (z,(N-min (L~ z)))) by REVROT_1:33;
 N-min (L~ z) in rng z by SPRECT_2:39;
then  (Rotate (z,(N-min (L~ z)))) /. 1 = N-min (L~ (Rotate (z,(N-min (L~ z))))) by A1, FINSEQ_6:92;
then A2: ( (N-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) < (N-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) & (N-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) < (W-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) ) by Lm7, SPRECT_2:68;
A3: W-min (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) by SPRECT_2:43;
assume A4: z /. 1 = W-min (L~ z) ; ::_thesis: (N-min (L~ z)) .. z < (N-max (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A5: Rotate ((Rotate (z,(N-min (L~ z)))),(W-min (L~ z))) = z by A4, REVROT_1:16;
 ( N-min (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) & N-max (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) ) by SPRECT_2:39, SPRECT_2:40;
hence  (N-min (L~ z)) .. z < (N-max (L~ z)) .. z by A1, A5, A3, A2, Th11; ::_thesis: verum
end;

theorem Th25: :: SPRECT_5:25
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = W-min (L~ z) & N-max (L~ z) <> E-max (L~ z) implies (N-max (L~ z)) .. z < (E-max (L~ z)) .. z )
set g = Rotate (z,(N-min (L~ z)));
A1: L~ z = L~ (Rotate (z,(N-min (L~ z)))) by REVROT_1:33;
 N-min (L~ z) in rng z by SPRECT_2:39;
then A2: (Rotate (z,(N-min (L~ z)))) /. 1 = N-min (L~ (Rotate (z,(N-min (L~ z))))) by A1, FINSEQ_6:92;
then A3: (E-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) < (W-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) by Lm3;
assume that
A4: z /. 1 = W-min (L~ z) and
A5: N-max (L~ z) <> E-max (L~ z) ; ::_thesis: (N-max (L~ z)) .. z < (E-max (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A6: Rotate ((Rotate (z,(N-min (L~ z)))),(W-min (L~ z))) = z by A4, REVROT_1:16;
A7: ( N-max (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) & E-max (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) ) by SPRECT_2:40, SPRECT_2:46;
 ( W-min (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) & (N-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) < (E-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) ) by A1, A5, A2, SPRECT_2:43, SPRECT_2:70;
hence  (N-max (L~ z)) .. z < (E-max (L~ z)) .. z by A1, A6, A7, A3, Th11; ::_thesis: verum
end;

theorem Th26: :: SPRECT_5:26
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = W-min (L~ z) implies (E-max (L~ z)) .. z < (E-min (L~ z)) .. z )
set g = Rotate (z,(N-min (L~ z)));
A1: L~ z = L~ (Rotate (z,(N-min (L~ z)))) by REVROT_1:33;
 N-min (L~ z) in rng z by SPRECT_2:39;
then  (Rotate (z,(N-min (L~ z)))) /. 1 = N-min (L~ (Rotate (z,(N-min (L~ z))))) by A1, FINSEQ_6:92;
then A2: ( (E-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) < (E-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) & (E-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) < (W-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) ) by Lm5, SPRECT_2:71;
A3: W-min (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) by SPRECT_2:43;
assume A4: z /. 1 = W-min (L~ z) ; ::_thesis: (E-max (L~ z)) .. z < (E-min (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A5: Rotate ((Rotate (z,(N-min (L~ z)))),(W-min (L~ z))) = z by A4, REVROT_1:16;
 ( E-min (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) & E-max (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) ) by SPRECT_2:45, SPRECT_2:46;
hence  (E-max (L~ z)) .. z < (E-min (L~ z)) .. z by A1, A5, A3, A2, Th11; ::_thesis: verum
end;

theorem Th27: :: SPRECT_5:27
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = W-min (L~ z) & E-min (L~ z) <> S-max (L~ z) implies (E-min (L~ z)) .. z < (S-max (L~ z)) .. z )
set g = Rotate (z,(N-min (L~ z)));
A1: L~ z = L~ (Rotate (z,(N-min (L~ z)))) by REVROT_1:33;
 N-min (L~ z) in rng z by SPRECT_2:39;
then A2: (Rotate (z,(N-min (L~ z)))) /. 1 = N-min (L~ (Rotate (z,(N-min (L~ z))))) by A1, FINSEQ_6:92;
then A3: (S-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) < (W-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) by Lm6;
assume that
A4: z /. 1 = W-min (L~ z) and
A5: E-min (L~ z) <> S-max (L~ z) ; ::_thesis: (E-min (L~ z)) .. z < (S-max (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A6: Rotate ((Rotate (z,(N-min (L~ z)))),(W-min (L~ z))) = z by A4, REVROT_1:16;
A7: ( E-min (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) & S-max (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) ) by SPRECT_2:42, SPRECT_2:45;
 ( W-min (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) & (E-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) < (S-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) ) by A1, A5, A2, SPRECT_2:43, SPRECT_2:72;
hence  (E-min (L~ z)) .. z < (S-max (L~ z)) .. z by A1, A6, A7, A3, Th11; ::_thesis: verum
end;

theorem :: SPRECT_5:28
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = W-min (L~ z) & S-min (L~ z) <> W-min (L~ z) implies (S-max (L~ z)) .. z < (S-min (L~ z)) .. z )
set g = Rotate (z,(N-min (L~ z)));
A1: L~ z = L~ (Rotate (z,(N-min (L~ z)))) by REVROT_1:33;
assume A2: z /. 1 = W-min (L~ z) ; ::_thesis: ( not S-min (L~ z) <> W-min (L~ z) or (S-max (L~ z)) .. z < (S-min (L~ z)) .. z )
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A3: Rotate ((Rotate (z,(N-min (L~ z)))),(W-min (L~ z))) = z by A2, REVROT_1:16;
A4: ( S-min (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) & S-max (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) ) by SPRECT_2:41, SPRECT_2:42;
 N-min (L~ z) in rng z by SPRECT_2:39;
then A5: (Rotate (z,(N-min (L~ z)))) /. 1 = N-min (L~ (Rotate (z,(N-min (L~ z))))) by A1, FINSEQ_6:92;
then A6: ( W-min (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) & (S-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) < (S-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) ) by SPRECT_2:43, SPRECT_2:73;
assume  S-min (L~ z) <> W-min (L~ z) ; ::_thesis: (S-max (L~ z)) .. z < (S-min (L~ z)) .. z
then  (S-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) < (W-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) by A1, A5, SPRECT_2:74;
hence  (S-max (L~ z)) .. z < (S-min (L~ z)) .. z by A1, A3, A4, A6, Th11; ::_thesis: verum
end;

theorem Th29: :: SPRECT_5:29
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
let f be non constant standard special_circular_sequence; ::_thesis: ( f /. 1 = S-max (L~ f) implies (S-max (L~ f)) .. f < (S-min (L~ f)) .. f )
assume  f /. 1 = S-max (L~ f) ; ::_thesis: (S-max (L~ f)) .. f < (S-min (L~ f)) .. f
then A1: (S-max (L~ f)) .. f = 1 by FINSEQ_6:43;
A2: S-min (L~ f) in rng f by SPRECT_2:41;
then  (S-min (L~ f)) .. f in dom f by FINSEQ_4:20;
then A3: (S-min (L~ f)) .. f >= 1 by FINSEQ_3:25;
 S-max (L~ f) in rng f by SPRECT_2:42;
then  (S-max (L~ f)) .. f <> (S-min (L~ f)) .. f by A2, FINSEQ_5:9, SPRECT_2:56;
hence  (S-max (L~ f)) .. f < (S-min (L~ f)) .. f by A3, A1, XXREAL_0:1; ::_thesis: verum
end;

theorem :: SPRECT_5:30
for f being non constant standard special_circular_sequence st f /. 1 = S-max (L~ f) holds
(S-min (L~ f)) .. f > 1
proof
let f be non constant standard special_circular_sequence; ::_thesis: ( f /. 1 = S-max (L~ f) implies (S-min (L~ f)) .. f > 1 )
assume A1: f /. 1 = S-max (L~ f) ; ::_thesis: (S-min (L~ f)) .. f > 1
then  (S-max (L~ f)) .. f = 1 by FINSEQ_6:43;
hence  (S-min (L~ f)) .. f > 1 by A1, Th29; ::_thesis: verum
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = W-min (L~ z) implies (E-max (L~ z)) .. z < (S-max (L~ z)) .. z )
assume A1: z /. 1 = W-min (L~ z) ; ::_thesis: (E-max (L~ z)) .. z < (S-max (L~ z)) .. z
then  (E-max (L~ z)) .. z < (E-min (L~ z)) .. z by Th26;
hence  (E-max (L~ z)) .. z < (S-max (L~ z)) .. z by A1, Th27, XXREAL_0:2; ::_thesis: verum
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = W-min (L~ z) implies (N-min (L~ z)) .. z < (E-max (L~ z)) .. z )
assume A1: z /. 1 = W-min (L~ z) ; ::_thesis: (N-min (L~ z)) .. z < (E-max (L~ z)) .. z
then  (N-min (L~ z)) .. z < (N-max (L~ z)) .. z by Th24;
hence  (N-min (L~ z)) .. z < (E-max (L~ z)) .. z by A1, Th25, XXREAL_0:2; ::_thesis: verum
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = W-min (L~ z) implies (N-min (L~ z)) .. z < (S-max (L~ z)) .. z )
assume A1: z /. 1 = W-min (L~ z) ; ::_thesis: (N-min (L~ z)) .. z < (S-max (L~ z)) .. z
then  (N-min (L~ z)) .. z < (E-max (L~ z)) .. z by Lm12;
hence  (N-min (L~ z)) .. z < (S-max (L~ z)) .. z by A1, Lm11, XXREAL_0:2; ::_thesis: verum
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = W-min (L~ z) implies (N-max (L~ z)) .. z < (S-max (L~ z)) .. z )
assume A1: z /. 1 = W-min (L~ z) ; ::_thesis: (N-max (L~ z)) .. z < (S-max (L~ z)) .. z
then  (E-max (L~ z)) .. z < (S-max (L~ z)) .. z by Lm11;
hence  (N-max (L~ z)) .. z < (S-max (L~ z)) .. z by A1, Th25, XXREAL_0:2; ::_thesis: verum
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = W-min (L~ z) implies (W-max (L~ z)) .. z < (S-max (L~ z)) .. z )
assume A1: z /. 1 = W-min (L~ z) ; ::_thesis: (W-max (L~ z)) .. z < (S-max (L~ z)) .. z
then  (N-min (L~ z)) .. z < (S-max (L~ z)) .. z by Lm13;
hence  (W-max (L~ z)) .. z < (S-max (L~ z)) .. z by A1, Th23, XXREAL_0:2; ::_thesis: verum
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = W-min (L~ z) implies (N-max (L~ z)) .. z < (E-min (L~ z)) .. z )
assume A1: z /. 1 = W-min (L~ z) ; ::_thesis: (N-max (L~ z)) .. z < (E-min (L~ z)) .. z
then  (E-max (L~ z)) .. z < (E-min (L~ z)) .. z by Th26;
hence  (N-max (L~ z)) .. z < (E-min (L~ z)) .. z by A1, Th25, XXREAL_0:2; ::_thesis: verum
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = W-min (L~ z) implies (N-min (L~ z)) .. z < (E-max (L~ z)) .. z )
assume A1: z /. 1 = W-min (L~ z) ; ::_thesis: (N-min (L~ z)) .. z < (E-max (L~ z)) .. z
then  (N-min (L~ z)) .. z < (N-max (L~ z)) .. z by Th24;
hence  (N-min (L~ z)) .. z < (E-max (L~ z)) .. z by A1, Th25, XXREAL_0:2; ::_thesis: verum
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = W-min (L~ z) implies (W-max (L~ z)) .. z < (E-max (L~ z)) .. z )
assume A1: z /. 1 = W-min (L~ z) ; ::_thesis: (W-max (L~ z)) .. z < (E-max (L~ z)) .. z
then  (W-max (L~ z)) .. z <= (N-min (L~ z)) .. z by Th23;
hence  (W-max (L~ z)) .. z < (E-max (L~ z)) .. z by A1, Lm17, XXREAL_0:2; ::_thesis: verum
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = W-min (L~ z) implies (W-max (L~ z)) .. z < (E-min (L~ z)) .. z )
assume A1: z /. 1 = W-min (L~ z) ; ::_thesis: (W-max (L~ z)) .. z < (E-min (L~ z)) .. z
then  (W-max (L~ z)) .. z < (E-max (L~ z)) .. z by Lm18;
hence  (W-max (L~ z)) .. z < (E-min (L~ z)) .. z by A1, Th26, XXREAL_0:2; ::_thesis: verum
end;

theorem Th31: :: SPRECT_5:31
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = S-max (L~ z) & S-min (L~ z) <> W-min (L~ z) implies (S-min (L~ z)) .. z < (W-min (L~ z)) .. z )
set g = Rotate (z,(N-min (L~ z)));
A1: L~ z = L~ (Rotate (z,(N-min (L~ z)))) by REVROT_1:33;
 N-min (L~ z) in rng z by SPRECT_2:39;
then A2: (Rotate (z,(N-min (L~ z)))) /. 1 = N-min (L~ (Rotate (z,(N-min (L~ z))))) by A1, FINSEQ_6:92;
then A3: ( S-min (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) & (S-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) < (S-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) ) by SPRECT_2:41, SPRECT_2:73;
assume that
A4: z /. 1 = S-max (L~ z) and
A5: S-min (L~ z) <> W-min (L~ z) ; ::_thesis: (S-min (L~ z)) .. z < (W-min (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A6: Rotate ((Rotate (z,(N-min (L~ z)))),(S-max (L~ z))) = z by A4, REVROT_1:16;
A7: ( W-min (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) & S-max (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) ) by SPRECT_2:42, SPRECT_2:43;
 (S-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) < (W-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) by A1, A5, A2, SPRECT_2:74;
hence  (S-min (L~ z)) .. z < (W-min (L~ z)) .. z by A1, A6, A7, A3, Th5; ::_thesis: verum
end;

theorem Th32: :: SPRECT_5:32
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = S-max (L~ z) implies (W-min (L~ z)) .. z < (W-max (L~ z)) .. z )
set g = Rotate (z,(W-min (L~ z)));
A1: L~ z = L~ (Rotate (z,(W-min (L~ z)))) by REVROT_1:33;
 W-min (L~ z) in rng z by SPRECT_2:43;
then  (Rotate (z,(W-min (L~ z)))) /. 1 = W-min (L~ (Rotate (z,(W-min (L~ z))))) by A1, FINSEQ_6:92;
then A2: ( (S-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) > (W-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) & (W-min (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) < (W-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) ) by Lm15, Th21;
A3: W-min (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) by SPRECT_2:43;
assume A4: z /. 1 = S-max (L~ z) ; ::_thesis: (W-min (L~ z)) .. z < (W-max (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A5: Rotate ((Rotate (z,(W-min (L~ z)))),(S-max (L~ z))) = z by A4, REVROT_1:16;
 ( S-max (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) & W-max (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) ) by SPRECT_2:42, SPRECT_2:44;
hence  (W-min (L~ z)) .. z < (W-max (L~ z)) .. z by A1, A5, A3, A2, Th11; ::_thesis: verum
end;

theorem Th33: :: SPRECT_5:33
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = S-max (L~ z) & W-max (L~ z) <> N-min (L~ z) implies (W-max (L~ z)) .. z < (N-min (L~ z)) .. z )
set g = Rotate (z,(W-min (L~ z)));
A1: L~ z = L~ (Rotate (z,(W-min (L~ z)))) by REVROT_1:33;
 W-min (L~ z) in rng z by SPRECT_2:43;
then A2: (Rotate (z,(W-min (L~ z)))) /. 1 = W-min (L~ (Rotate (z,(W-min (L~ z))))) by A1, FINSEQ_6:92;
then A3: (N-min (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) < (S-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) by Lm13;
assume that
A4: z /. 1 = S-max (L~ z) and
A5: W-max (L~ z) <> N-min (L~ z) ; ::_thesis: (W-max (L~ z)) .. z < (N-min (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A6: Rotate ((Rotate (z,(W-min (L~ z)))),(S-max (L~ z))) = z by A4, REVROT_1:16;
A7: ( W-max (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) & N-min (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) ) by SPRECT_2:39, SPRECT_2:44;
 ( S-max (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) & (W-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) < (N-min (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) ) by A1, A5, A2, Th23, SPRECT_2:42;
hence  (W-max (L~ z)) .. z < (N-min (L~ z)) .. z by A1, A6, A7, A3, Th11; ::_thesis: verum
end;

theorem Th34: :: SPRECT_5:34
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = S-max (L~ z) implies (N-min (L~ z)) .. z < (N-max (L~ z)) .. z )
set g = Rotate (z,(W-min (L~ z)));
A1: L~ z = L~ (Rotate (z,(W-min (L~ z)))) by REVROT_1:33;
 W-min (L~ z) in rng z by SPRECT_2:43;
then  (Rotate (z,(W-min (L~ z)))) /. 1 = W-min (L~ (Rotate (z,(W-min (L~ z))))) by A1, FINSEQ_6:92;
then A2: ( (N-min (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) < (N-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) & (N-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) < (S-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) ) by Lm14, Th24;
A3: S-max (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) by SPRECT_2:42;
assume A4: z /. 1 = S-max (L~ z) ; ::_thesis: (N-min (L~ z)) .. z < (N-max (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A5: Rotate ((Rotate (z,(W-min (L~ z)))),(S-max (L~ z))) = z by A4, REVROT_1:16;
 ( N-max (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) & N-min (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) ) by SPRECT_2:39, SPRECT_2:40;
hence  (N-min (L~ z)) .. z < (N-max (L~ z)) .. z by A1, A5, A3, A2, Th11; ::_thesis: verum
end;

theorem Th35: :: SPRECT_5:35
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = S-max (L~ z) & N-max (L~ z) <> E-max (L~ z) implies (N-max (L~ z)) .. z < (E-max (L~ z)) .. z )
set g = Rotate (z,(W-min (L~ z)));
A1: L~ z = L~ (Rotate (z,(W-min (L~ z)))) by REVROT_1:33;
 W-min (L~ z) in rng z by SPRECT_2:43;
then A2: (Rotate (z,(W-min (L~ z)))) /. 1 = W-min (L~ (Rotate (z,(W-min (L~ z))))) by A1, FINSEQ_6:92;
then A3: (E-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) < (S-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) by Lm11;
assume that
A4: z /. 1 = S-max (L~ z) and
A5: N-max (L~ z) <> E-max (L~ z) ; ::_thesis: (N-max (L~ z)) .. z < (E-max (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A6: Rotate ((Rotate (z,(W-min (L~ z)))),(S-max (L~ z))) = z by A4, REVROT_1:16;
A7: ( N-max (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) & E-max (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) ) by SPRECT_2:40, SPRECT_2:46;
 ( S-max (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) & (N-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) < (E-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) ) by A1, A5, A2, Th25, SPRECT_2:42;
hence  (N-max (L~ z)) .. z < (E-max (L~ z)) .. z by A1, A6, A7, A3, Th11; ::_thesis: verum
end;

theorem :: SPRECT_5:36
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = S-max (L~ z) & E-min (L~ z) <> S-max (L~ z) implies (E-max (L~ z)) .. z < (E-min (L~ z)) .. z )
set g = Rotate (z,(W-min (L~ z)));
A1: L~ z = L~ (Rotate (z,(W-min (L~ z)))) by REVROT_1:33;
assume A2: z /. 1 = S-max (L~ z) ; ::_thesis: ( not E-min (L~ z) <> S-max (L~ z) or (E-max (L~ z)) .. z < (E-min (L~ z)) .. z )
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A3: Rotate ((Rotate (z,(W-min (L~ z)))),(S-max (L~ z))) = z by A2, REVROT_1:16;
A4: ( E-min (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) & E-max (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) ) by SPRECT_2:45, SPRECT_2:46;
 W-min (L~ z) in rng z by SPRECT_2:43;
then A5: (Rotate (z,(W-min (L~ z)))) /. 1 = W-min (L~ (Rotate (z,(W-min (L~ z))))) by A1, FINSEQ_6:92;
then A6: ( S-max (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) & (E-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) < (E-min (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) ) by Th26, SPRECT_2:42;
assume  E-min (L~ z) <> S-max (L~ z) ; ::_thesis: (E-max (L~ z)) .. z < (E-min (L~ z)) .. z
then  (E-min (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) < (S-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) by A1, A5, Th27;
hence  (E-max (L~ z)) .. z < (E-min (L~ z)) .. z by A1, A3, A4, A6, Th11; ::_thesis: verum
end;

theorem Th37: :: SPRECT_5:37
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
let f be non constant standard special_circular_sequence; ::_thesis: ( f /. 1 = E-max (L~ f) implies (E-max (L~ f)) .. f < (E-min (L~ f)) .. f )
assume  f /. 1 = E-max (L~ f) ; ::_thesis: (E-max (L~ f)) .. f < (E-min (L~ f)) .. f
then A1: (E-max (L~ f)) .. f = 1 by FINSEQ_6:43;
A2: E-min (L~ f) in rng f by SPRECT_2:45;
then  (E-min (L~ f)) .. f in dom f by FINSEQ_4:20;
then A3: (E-min (L~ f)) .. f >= 1 by FINSEQ_3:25;
 E-max (L~ f) in rng f by SPRECT_2:46;
then  (E-min (L~ f)) .. f <> (E-max (L~ f)) .. f by A2, FINSEQ_5:9, SPRECT_2:54;
hence  (E-max (L~ f)) .. f < (E-min (L~ f)) .. f by A3, A1, XXREAL_0:1; ::_thesis: verum
end;

theorem :: SPRECT_5:38
for f being non constant standard special_circular_sequence st f /. 1 = E-max (L~ f) holds
(E-min (L~ f)) .. f > 1
proof
let f be non constant standard special_circular_sequence; ::_thesis: ( f /. 1 = E-max (L~ f) implies (E-min (L~ f)) .. f > 1 )
assume A1: f /. 1 = E-max (L~ f) ; ::_thesis: (E-min (L~ f)) .. f > 1
then  (E-max (L~ f)) .. f = 1 by FINSEQ_6:43;
hence  (E-min (L~ f)) .. f > 1 by A1, Th37; ::_thesis: verum
end;

theorem Th39: :: SPRECT_5:39
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = E-max (L~ z) & S-max (L~ z) <> E-min (L~ z) implies (E-min (L~ z)) .. z < (S-max (L~ z)) .. z )
set g = Rotate (z,(N-min (L~ z)));
A1: L~ z = L~ (Rotate (z,(N-min (L~ z)))) by REVROT_1:33;
 N-min (L~ z) in rng z by SPRECT_2:39;
then A2: (Rotate (z,(N-min (L~ z)))) /. 1 = N-min (L~ (Rotate (z,(N-min (L~ z))))) by A1, FINSEQ_6:92;
then A3: ( E-min (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) & (E-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) < (E-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) ) by SPRECT_2:45, SPRECT_2:71;
assume that
A4: z /. 1 = E-max (L~ z) and
A5: S-max (L~ z) <> E-min (L~ z) ; ::_thesis: (E-min (L~ z)) .. z < (S-max (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A6: Rotate ((Rotate (z,(N-min (L~ z)))),(E-max (L~ z))) = z by A4, REVROT_1:16;
A7: ( S-max (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) & E-max (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) ) by SPRECT_2:42, SPRECT_2:46;
 (E-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) < (S-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) by A1, A5, A2, SPRECT_2:72;
hence  (E-min (L~ z)) .. z < (S-max (L~ z)) .. z by A1, A6, A7, A3, Th5; ::_thesis: verum
end;

theorem Th40: :: SPRECT_5:40
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = E-max (L~ z) implies (S-max (L~ z)) .. z < (S-min (L~ z)) .. z )
set g = Rotate (z,(N-min (L~ z)));
A1: L~ z = L~ (Rotate (z,(N-min (L~ z)))) by REVROT_1:33;
 N-min (L~ z) in rng z by SPRECT_2:39;
then  (Rotate (z,(N-min (L~ z)))) /. 1 = N-min (L~ (Rotate (z,(N-min (L~ z))))) by A1, FINSEQ_6:92;
then A2: ( (E-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) < (S-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) & (S-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) < (S-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) ) by Lm1, SPRECT_2:73;
A3: S-min (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) by SPRECT_2:41;
assume A4: z /. 1 = E-max (L~ z) ; ::_thesis: (S-max (L~ z)) .. z < (S-min (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A5: Rotate ((Rotate (z,(N-min (L~ z)))),(E-max (L~ z))) = z by A4, REVROT_1:16;
 ( S-max (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) & E-max (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) ) by SPRECT_2:42, SPRECT_2:46;
hence  (S-max (L~ z)) .. z < (S-min (L~ z)) .. z by A1, A5, A3, A2, Th5; ::_thesis: verum
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = S-max (L~ z) implies (N-min (L~ z)) .. z < (E-max (L~ z)) .. z )
assume A1: z /. 1 = S-max (L~ z) ; ::_thesis: (N-min (L~ z)) .. z < (E-max (L~ z)) .. z
then  (N-min (L~ z)) .. z < (N-max (L~ z)) .. z by Th34;
hence  (N-min (L~ z)) .. z < (E-max (L~ z)) .. z by A1, Th35, XXREAL_0:2; ::_thesis: verum
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = S-max (L~ z) implies (W-max (L~ z)) .. z < (E-max (L~ z)) .. z )
assume A1: z /. 1 = S-max (L~ z) ; ::_thesis: (W-max (L~ z)) .. z < (E-max (L~ z)) .. z
then  (N-min (L~ z)) .. z < (E-max (L~ z)) .. z by Lm20;
hence  (W-max (L~ z)) .. z < (E-max (L~ z)) .. z by A1, Th33, XXREAL_0:2; ::_thesis: verum
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = S-max (L~ z) implies (W-min (L~ z)) .. z < (E-max (L~ z)) .. z )
assume A1: z /. 1 = S-max (L~ z) ; ::_thesis: (W-min (L~ z)) .. z < (E-max (L~ z)) .. z
then  (W-min (L~ z)) .. z < (W-max (L~ z)) .. z by Th32;
hence  (W-min (L~ z)) .. z < (E-max (L~ z)) .. z by A1, Lm21, XXREAL_0:2; ::_thesis: verum
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = S-max (L~ z) implies (W-max (L~ z)) .. z < (N-max (L~ z)) .. z )
assume A1: z /. 1 = S-max (L~ z) ; ::_thesis: (W-max (L~ z)) .. z < (N-max (L~ z)) .. z
then  (N-min (L~ z)) .. z < (N-max (L~ z)) .. z by Th34;
hence  (W-max (L~ z)) .. z < (N-max (L~ z)) .. z by A1, Th33, XXREAL_0:2; ::_thesis: verum
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = S-max (L~ z) implies (W-min (L~ z)) .. z < (N-min (L~ z)) .. z )
assume A1: z /. 1 = S-max (L~ z) ; ::_thesis: (W-min (L~ z)) .. z < (N-min (L~ z)) .. z
then  (W-min (L~ z)) .. z < (W-max (L~ z)) .. z by Th32;
hence  (W-min (L~ z)) .. z < (N-min (L~ z)) .. z by A1, Th33, XXREAL_0:2; ::_thesis: verum
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = S-max (L~ z) implies (S-min (L~ z)) .. z < (N-min (L~ z)) .. z )
assume A1: z /. 1 = S-max (L~ z) ; ::_thesis: (S-min (L~ z)) .. z < (N-min (L~ z)) .. z
then  (S-min (L~ z)) .. z <= (W-min (L~ z)) .. z by Th31;
hence  (S-min (L~ z)) .. z < (N-min (L~ z)) .. z by A1, Lm24, XXREAL_0:2; ::_thesis: verum
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = S-max (L~ z) implies (S-min (L~ z)) .. z < (N-max (L~ z)) .. z )
assume A1: z /. 1 = S-max (L~ z) ; ::_thesis: (S-min (L~ z)) .. z < (N-max (L~ z)) .. z
then  (S-min (L~ z)) .. z < (N-min (L~ z)) .. z by Lm25;
hence  (S-min (L~ z)) .. z < (N-max (L~ z)) .. z by A1, Th34, XXREAL_0:2; ::_thesis: verum
end;

theorem Th41: :: SPRECT_5:41
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = E-max (L~ z) & S-min (L~ z) <> W-min (L~ z) implies (S-min (L~ z)) .. z < (W-min (L~ z)) .. z )
set g = Rotate (z,(S-max (L~ z)));
A1: L~ z = L~ (Rotate (z,(S-max (L~ z)))) by REVROT_1:33;
 S-max (L~ z) in rng z by SPRECT_2:42;
then A2: (Rotate (z,(S-max (L~ z)))) /. 1 = S-max (L~ (Rotate (z,(S-max (L~ z))))) by A1, FINSEQ_6:92;
then A3: (W-min (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) < (E-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) by Lm22;
assume that
A4: z /. 1 = E-max (L~ z) and
A5: S-min (L~ z) <> W-min (L~ z) ; ::_thesis: (S-min (L~ z)) .. z < (W-min (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A6: Rotate ((Rotate (z,(S-max (L~ z)))),(E-max (L~ z))) = z by A4, REVROT_1:16;
A7: ( S-min (L~ (Rotate (z,(S-max (L~ z))))) in rng (Rotate (z,(S-max (L~ z)))) & W-min (L~ (Rotate (z,(S-max (L~ z))))) in rng (Rotate (z,(S-max (L~ z)))) ) by SPRECT_2:41, SPRECT_2:43;
 ( E-max (L~ (Rotate (z,(S-max (L~ z))))) in rng (Rotate (z,(S-max (L~ z)))) & (S-min (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) < (W-min (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) ) by A1, A5, A2, Th31, SPRECT_2:46;
hence  (S-min (L~ z)) .. z < (W-min (L~ z)) .. z by A1, A6, A7, A3, Th11; ::_thesis: verum
end;

theorem Th42: :: SPRECT_5:42
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = E-max (L~ z) implies (W-min (L~ z)) .. z < (W-max (L~ z)) .. z )
set g = Rotate (z,(S-max (L~ z)));
A1: L~ z = L~ (Rotate (z,(S-max (L~ z)))) by REVROT_1:33;
 S-max (L~ z) in rng z by SPRECT_2:42;
then  (Rotate (z,(S-max (L~ z)))) /. 1 = S-max (L~ (Rotate (z,(S-max (L~ z))))) by A1, FINSEQ_6:92;
then A2: ( (W-min (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) < (W-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) & (W-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) < (E-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) ) by Lm21, Th32;
A3: E-max (L~ (Rotate (z,(S-max (L~ z))))) in rng (Rotate (z,(S-max (L~ z)))) by SPRECT_2:46;
assume A4: z /. 1 = E-max (L~ z) ; ::_thesis: (W-min (L~ z)) .. z < (W-max (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A5: Rotate ((Rotate (z,(S-max (L~ z)))),(E-max (L~ z))) = z by A4, REVROT_1:16;
 ( W-max (L~ (Rotate (z,(S-max (L~ z))))) in rng (Rotate (z,(S-max (L~ z)))) & W-min (L~ (Rotate (z,(S-max (L~ z))))) in rng (Rotate (z,(S-max (L~ z)))) ) by SPRECT_2:43, SPRECT_2:44;
hence  (W-min (L~ z)) .. z < (W-max (L~ z)) .. z by A1, A5, A3, A2, Th11; ::_thesis: verum
end;

theorem Th43: :: SPRECT_5:43
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = E-max (L~ z) & W-max (L~ z) <> N-min (L~ z) implies (W-max (L~ z)) .. z < (N-min (L~ z)) .. z )
set g = Rotate (z,(S-max (L~ z)));
A1: L~ z = L~ (Rotate (z,(S-max (L~ z)))) by REVROT_1:33;
 S-max (L~ z) in rng z by SPRECT_2:42;
then A2: (Rotate (z,(S-max (L~ z)))) /. 1 = S-max (L~ (Rotate (z,(S-max (L~ z))))) by A1, FINSEQ_6:92;
then A3: (N-min (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) < (E-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) by Lm20;
assume that
A4: z /. 1 = E-max (L~ z) and
A5: W-max (L~ z) <> N-min (L~ z) ; ::_thesis: (W-max (L~ z)) .. z < (N-min (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A6: Rotate ((Rotate (z,(S-max (L~ z)))),(E-max (L~ z))) = z by A4, REVROT_1:16;
A7: ( W-max (L~ (Rotate (z,(S-max (L~ z))))) in rng (Rotate (z,(S-max (L~ z)))) & N-min (L~ (Rotate (z,(S-max (L~ z))))) in rng (Rotate (z,(S-max (L~ z)))) ) by SPRECT_2:39, SPRECT_2:44;
 ( E-max (L~ (Rotate (z,(S-max (L~ z))))) in rng (Rotate (z,(S-max (L~ z)))) & (W-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) < (N-min (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) ) by A1, A5, A2, Th33, SPRECT_2:46;
hence  (W-max (L~ z)) .. z < (N-min (L~ z)) .. z by A1, A6, A7, A3, Th11; ::_thesis: verum
end;

theorem :: SPRECT_5:44
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = E-max (L~ z) & N-max (L~ z) <> E-max (L~ z) implies (N-min (L~ z)) .. z < (N-max (L~ z)) .. z )
set g = Rotate (z,(S-max (L~ z)));
A1: L~ z = L~ (Rotate (z,(S-max (L~ z)))) by REVROT_1:33;
assume A2: z /. 1 = E-max (L~ z) ; ::_thesis: ( not N-max (L~ z) <> E-max (L~ z) or (N-min (L~ z)) .. z < (N-max (L~ z)) .. z )
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A3: Rotate ((Rotate (z,(S-max (L~ z)))),(E-max (L~ z))) = z by A2, REVROT_1:16;
A4: ( N-max (L~ (Rotate (z,(S-max (L~ z))))) in rng (Rotate (z,(S-max (L~ z)))) & N-min (L~ (Rotate (z,(S-max (L~ z))))) in rng (Rotate (z,(S-max (L~ z)))) ) by SPRECT_2:39, SPRECT_2:40;
 S-max (L~ z) in rng z by SPRECT_2:42;
then A5: (Rotate (z,(S-max (L~ z)))) /. 1 = S-max (L~ (Rotate (z,(S-max (L~ z))))) by A1, FINSEQ_6:92;
then A6: ( E-max (L~ (Rotate (z,(S-max (L~ z))))) in rng (Rotate (z,(S-max (L~ z)))) & (N-min (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) < (N-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) ) by Th34, SPRECT_2:46;
assume  N-max (L~ z) <> E-max (L~ z) ; ::_thesis: (N-min (L~ z)) .. z < (N-max (L~ z)) .. z
then  (N-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) < (E-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) by A1, A5, Th35;
hence  (N-min (L~ z)) .. z < (N-max (L~ z)) .. z by A1, A3, A4, A6, Th11; ::_thesis: verum
end;

theorem :: SPRECT_5:45
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
let f be non constant standard special_circular_sequence; ::_thesis: ( f /. 1 = N-max (L~ f) & N-max (L~ f) <> E-max (L~ f) implies (N-max (L~ f)) .. f < (E-max (L~ f)) .. f )
assume that
A1: f /. 1 = N-max (L~ f) and
A2: N-max (L~ f) <> E-max (L~ f) ; ::_thesis: (N-max (L~ f)) .. f < (E-max (L~ f)) .. f
A3: E-max (L~ f) in rng f by SPRECT_2:46;
then  (E-max (L~ f)) .. f in dom f by FINSEQ_4:20;
then A4: (E-max (L~ f)) .. f >= 1 by FINSEQ_3:25;
 ( N-max (L~ f) in rng f & (N-max (L~ f)) .. f = 1 ) by A1, FINSEQ_6:43, SPRECT_2:40;
hence  (N-max (L~ f)) .. f < (E-max (L~ f)) .. f by A3, A2, A4, FINSEQ_5:9, XXREAL_0:1; ::_thesis: verum
end;

theorem :: SPRECT_5:46
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = N-max (L~ z) implies (E-max (L~ z)) .. z < (E-min (L~ z)) .. z )
set g = Rotate (z,(W-min (L~ z)));
A1: L~ z = L~ (Rotate (z,(W-min (L~ z)))) by REVROT_1:33;
 W-min (L~ z) in rng z by SPRECT_2:43;
then  (Rotate (z,(W-min (L~ z)))) /. 1 = W-min (L~ (Rotate (z,(W-min (L~ z))))) by A1, FINSEQ_6:92;
then A2: ( (N-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) <= (E-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) & (E-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) < (E-min (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) ) by Th25, Th26;
A3: E-max (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) by SPRECT_2:46;
assume A4: z /. 1 = N-max (L~ z) ; ::_thesis: (E-max (L~ z)) .. z < (E-min (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A5: Rotate ((Rotate (z,(W-min (L~ z)))),(N-max (L~ z))) = z by A4, REVROT_1:16;
 ( E-min (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) & N-max (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) ) by SPRECT_2:40, SPRECT_2:45;
hence  (E-max (L~ z)) .. z < (E-min (L~ z)) .. z by A1, A5, A3, A2, Th5; ::_thesis: verum
end;

theorem :: SPRECT_5:47
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = N-max (L~ z) & E-min (L~ z) <> S-max (L~ z) implies (E-min (L~ z)) .. z < (S-max (L~ z)) .. z )
set g = Rotate (z,(W-min (L~ z)));
A1: L~ z = L~ (Rotate (z,(W-min (L~ z)))) by REVROT_1:33;
 W-min (L~ z) in rng z by SPRECT_2:43;
then A2: (Rotate (z,(W-min (L~ z)))) /. 1 = W-min (L~ (Rotate (z,(W-min (L~ z))))) by A1, FINSEQ_6:92;
then A3: ( S-max (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) & (N-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) < (E-min (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) ) by Lm16, SPRECT_2:42;
assume that
A4: z /. 1 = N-max (L~ z) and
A5: E-min (L~ z) <> S-max (L~ z) ; ::_thesis: (E-min (L~ z)) .. z < (S-max (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A6: Rotate ((Rotate (z,(W-min (L~ z)))),(N-max (L~ z))) = z by A4, REVROT_1:16;
A7: ( E-min (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) & N-max (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) ) by SPRECT_2:40, SPRECT_2:45;
 (E-min (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) < (S-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) by A1, A5, A2, Th27;
hence  (E-min (L~ z)) .. z < (S-max (L~ z)) .. z by A1, A6, A7, A3, Th5; ::_thesis: verum
end;

theorem :: SPRECT_5:48
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = N-max (L~ z) implies (S-max (L~ z)) .. z < (S-min (L~ z)) .. z )
set g = Rotate (z,(N-min (L~ z)));
A1: L~ z = L~ (Rotate (z,(N-min (L~ z)))) by REVROT_1:33;
 N-min (L~ z) in rng z by SPRECT_2:39;
then  (Rotate (z,(N-min (L~ z)))) /. 1 = N-min (L~ (Rotate (z,(N-min (L~ z))))) by A1, FINSEQ_6:92;
then A2: ( (S-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) < (S-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) & (N-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) < (S-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) ) by Lm9, SPRECT_2:73;
A3: N-max (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) by SPRECT_2:40;
assume A4: z /. 1 = N-max (L~ z) ; ::_thesis: (S-max (L~ z)) .. z < (S-min (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A5: Rotate ((Rotate (z,(N-min (L~ z)))),(N-max (L~ z))) = z by A4, REVROT_1:16;
 ( S-max (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) & S-min (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) ) by SPRECT_2:41, SPRECT_2:42;
hence  (S-max (L~ z)) .. z < (S-min (L~ z)) .. z by A1, A5, A3, A2, Th5; ::_thesis: verum
end;

theorem :: SPRECT_5:49
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = N-max (L~ z) & S-min (L~ z) <> W-min (L~ z) implies (S-min (L~ z)) .. z < (W-min (L~ z)) .. z )
set g = Rotate (z,(N-min (L~ z)));
A1: L~ z = L~ (Rotate (z,(N-min (L~ z)))) by REVROT_1:33;
 N-min (L~ z) in rng z by SPRECT_2:39;
then A2: (Rotate (z,(N-min (L~ z)))) /. 1 = N-min (L~ (Rotate (z,(N-min (L~ z))))) by A1, FINSEQ_6:92;
then A3: (N-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) < (S-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) by Lm10;
assume that
A4: z /. 1 = N-max (L~ z) and
A5: S-min (L~ z) <> W-min (L~ z) ; ::_thesis: (S-min (L~ z)) .. z < (W-min (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A6: Rotate ((Rotate (z,(N-min (L~ z)))),(N-max (L~ z))) = z by A4, REVROT_1:16;
A7: ( W-min (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) & S-min (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) ) by SPRECT_2:41, SPRECT_2:43;
 ( N-max (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) & (S-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) < (W-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) ) by A1, A5, A2, SPRECT_2:40, SPRECT_2:74;
hence  (S-min (L~ z)) .. z < (W-min (L~ z)) .. z by A1, A6, A7, A3, Th5; ::_thesis: verum
end;

theorem :: SPRECT_5:50
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = N-max (L~ z) implies (W-min (L~ z)) .. z < (W-max (L~ z)) .. z )
set g = Rotate (z,(S-max (L~ z)));
A1: L~ z = L~ (Rotate (z,(S-max (L~ z)))) by REVROT_1:33;
 S-max (L~ z) in rng z by SPRECT_2:42;
then  (Rotate (z,(S-max (L~ z)))) /. 1 = S-max (L~ (Rotate (z,(S-max (L~ z))))) by A1, FINSEQ_6:92;
then A2: ( (W-min (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) < (W-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) & (W-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) < (N-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) ) by Lm23, Th32;
A3: N-max (L~ (Rotate (z,(S-max (L~ z))))) in rng (Rotate (z,(S-max (L~ z)))) by SPRECT_2:40;
assume A4: z /. 1 = N-max (L~ z) ; ::_thesis: (W-min (L~ z)) .. z < (W-max (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A5: Rotate ((Rotate (z,(S-max (L~ z)))),(N-max (L~ z))) = z by A4, REVROT_1:16;
 ( W-min (L~ (Rotate (z,(S-max (L~ z))))) in rng (Rotate (z,(S-max (L~ z)))) & W-max (L~ (Rotate (z,(S-max (L~ z))))) in rng (Rotate (z,(S-max (L~ z)))) ) by SPRECT_2:43, SPRECT_2:44;
hence  (W-min (L~ z)) .. z < (W-max (L~ z)) .. z by A1, A5, A3, A2, Th11; ::_thesis: verum
end;

theorem :: SPRECT_5:51
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = N-max (L~ z) & N-min (L~ z) <> W-max (L~ z) implies (W-max (L~ z)) .. z < (N-min (L~ z)) .. z )
set g = Rotate (z,(S-max (L~ z)));
A1: L~ z = L~ (Rotate (z,(S-max (L~ z)))) by REVROT_1:33;
 S-max (L~ z) in rng z by SPRECT_2:42;
then A2: (Rotate (z,(S-max (L~ z)))) /. 1 = S-max (L~ (Rotate (z,(S-max (L~ z))))) by A1, FINSEQ_6:92;
then A3: (N-min (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) < (N-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) by Th34;
assume that
A4: z /. 1 = N-max (L~ z) and
A5: N-min (L~ z) <> W-max (L~ z) ; ::_thesis: (W-max (L~ z)) .. z < (N-min (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A6: Rotate ((Rotate (z,(S-max (L~ z)))),(N-max (L~ z))) = z by A4, REVROT_1:16;
A7: ( N-min (L~ (Rotate (z,(S-max (L~ z))))) in rng (Rotate (z,(S-max (L~ z)))) & W-max (L~ (Rotate (z,(S-max (L~ z))))) in rng (Rotate (z,(S-max (L~ z)))) ) by SPRECT_2:39, SPRECT_2:44;
 ( N-max (L~ (Rotate (z,(S-max (L~ z))))) in rng (Rotate (z,(S-max (L~ z)))) & (W-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) < (N-min (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) ) by A1, A5, A2, Th33, SPRECT_2:40;
hence  (W-max (L~ z)) .. z < (N-min (L~ z)) .. z by A1, A6, A7, A3, Th11; ::_thesis: verum
end;

theorem :: SPRECT_5:52
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
let f be non constant standard special_circular_sequence; ::_thesis: ( f /. 1 = E-min (L~ f) & E-min (L~ f) <> S-max (L~ f) implies (E-min (L~ f)) .. f < (S-max (L~ f)) .. f )
assume that
A1: f /. 1 = E-min (L~ f) and
A2: E-min (L~ f) <> S-max (L~ f) ; ::_thesis: (E-min (L~ f)) .. f < (S-max (L~ f)) .. f
A3: S-max (L~ f) in rng f by SPRECT_2:42;
then  (S-max (L~ f)) .. f in dom f by FINSEQ_4:20;
then A4: (S-max (L~ f)) .. f >= 1 by FINSEQ_3:25;
 ( E-min (L~ f) in rng f & (E-min (L~ f)) .. f = 1 ) by A1, FINSEQ_6:43, SPRECT_2:45;
hence  (E-min (L~ f)) .. f < (S-max (L~ f)) .. f by A3, A2, A4, FINSEQ_5:9, XXREAL_0:1; ::_thesis: verum
end;

theorem :: SPRECT_5:53
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = E-min (L~ z) implies (S-max (L~ z)) .. z < (S-min (L~ z)) .. z )
set g = Rotate (z,(N-min (L~ z)));
A1: L~ z = L~ (Rotate (z,(N-min (L~ z)))) by REVROT_1:33;
 N-min (L~ z) in rng z by SPRECT_2:39;
then  (Rotate (z,(N-min (L~ z)))) /. 1 = N-min (L~ (Rotate (z,(N-min (L~ z))))) by A1, FINSEQ_6:92;
then A2: ( (E-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) <= (S-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) & (S-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) < (S-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) ) by SPRECT_2:72, SPRECT_2:73;
A3: S-max (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) by SPRECT_2:42;
assume A4: z /. 1 = E-min (L~ z) ; ::_thesis: (S-max (L~ z)) .. z < (S-min (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A5: Rotate ((Rotate (z,(N-min (L~ z)))),(E-min (L~ z))) = z by A4, REVROT_1:16;
 ( S-min (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) & E-min (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) ) by SPRECT_2:41, SPRECT_2:45;
hence  (S-max (L~ z)) .. z < (S-min (L~ z)) .. z by A1, A5, A3, A2, Th5; ::_thesis: verum
end;

theorem :: SPRECT_5:54
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = E-min (L~ z) & S-min (L~ z) <> W-min (L~ z) implies (S-min (L~ z)) .. z < (W-min (L~ z)) .. z )
set g = Rotate (z,(N-min (L~ z)));
A1: L~ z = L~ (Rotate (z,(N-min (L~ z)))) by REVROT_1:33;
 N-min (L~ z) in rng z by SPRECT_2:39;
then A2: (Rotate (z,(N-min (L~ z)))) /. 1 = N-min (L~ (Rotate (z,(N-min (L~ z))))) by A1, FINSEQ_6:92;
then A3: ( W-min (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) & (E-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) < (S-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) ) by Lm4, SPRECT_2:43;
assume that
A4: z /. 1 = E-min (L~ z) and
A5: S-min (L~ z) <> W-min (L~ z) ; ::_thesis: (S-min (L~ z)) .. z < (W-min (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A6: Rotate ((Rotate (z,(N-min (L~ z)))),(E-min (L~ z))) = z by A4, REVROT_1:16;
A7: ( S-min (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) & E-min (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) ) by SPRECT_2:41, SPRECT_2:45;
 (S-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) < (W-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) by A1, A5, A2, SPRECT_2:74;
hence  (S-min (L~ z)) .. z < (W-min (L~ z)) .. z by A1, A6, A7, A3, Th5; ::_thesis: verum
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = E-max (L~ z) implies (S-max (L~ z)) .. z < (W-min (L~ z)) .. z )
assume A1: z /. 1 = E-max (L~ z) ; ::_thesis: (S-max (L~ z)) .. z < (W-min (L~ z)) .. z
then  (S-max (L~ z)) .. z < (S-min (L~ z)) .. z by Th40;
hence  (S-max (L~ z)) .. z < (W-min (L~ z)) .. z by A1, Th41, XXREAL_0:2; ::_thesis: verum
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = E-max (L~ z) implies (E-min (L~ z)) .. z < (W-min (L~ z)) .. z )
assume A1: z /. 1 = E-max (L~ z) ; ::_thesis: (E-min (L~ z)) .. z < (W-min (L~ z)) .. z
then  (E-min (L~ z)) .. z <= (S-max (L~ z)) .. z by Th39;
hence  (E-min (L~ z)) .. z < (W-min (L~ z)) .. z by A1, Lm27, XXREAL_0:2; ::_thesis: verum
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = E-max (L~ z) implies (E-min (L~ z)) .. z < (W-max (L~ z)) .. z )
assume A1: z /. 1 = E-max (L~ z) ; ::_thesis: (E-min (L~ z)) .. z < (W-max (L~ z)) .. z
then  (E-min (L~ z)) .. z < (W-min (L~ z)) .. z by Lm28;
hence  (E-min (L~ z)) .. z < (W-max (L~ z)) .. z by A1, Th42, XXREAL_0:2; ::_thesis: verum
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = E-max (L~ z) implies (S-min (L~ z)) .. z < (W-max (L~ z)) .. z )
assume A1: z /. 1 = E-max (L~ z) ; ::_thesis: (S-min (L~ z)) .. z < (W-max (L~ z)) .. z
then  (W-min (L~ z)) .. z < (W-max (L~ z)) .. z by Th42;
hence  (S-min (L~ z)) .. z < (W-max (L~ z)) .. z by A1, Th41, XXREAL_0:2; ::_thesis: verum
end;

theorem :: SPRECT_5:55
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = E-min (L~ z) implies (W-min (L~ z)) .. z < (W-max (L~ z)) .. z )
set g = Rotate (z,(E-max (L~ z)));
A1: L~ z = L~ (Rotate (z,(E-max (L~ z)))) by REVROT_1:33;
 E-max (L~ z) in rng z by SPRECT_2:46;
then  (Rotate (z,(E-max (L~ z)))) /. 1 = E-max (L~ (Rotate (z,(E-max (L~ z))))) by A1, FINSEQ_6:92;
then A2: ( (W-min (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) < (W-max (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) & (E-min (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) < (W-min (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) ) by Lm28, Th42;
A3: E-min (L~ (Rotate (z,(E-max (L~ z))))) in rng (Rotate (z,(E-max (L~ z)))) by SPRECT_2:45;
assume A4: z /. 1 = E-min (L~ z) ; ::_thesis: (W-min (L~ z)) .. z < (W-max (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A5: Rotate ((Rotate (z,(E-max (L~ z)))),(E-min (L~ z))) = z by A4, REVROT_1:16;
 ( W-min (L~ (Rotate (z,(E-max (L~ z))))) in rng (Rotate (z,(E-max (L~ z)))) & W-max (L~ (Rotate (z,(E-max (L~ z))))) in rng (Rotate (z,(E-max (L~ z)))) ) by SPRECT_2:43, SPRECT_2:44;
hence  (W-min (L~ z)) .. z < (W-max (L~ z)) .. z by A1, A5, A3, A2, Th5; ::_thesis: verum
end;

theorem :: SPRECT_5:56
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = E-min (L~ z) & W-max (L~ z) <> N-min (L~ z) implies (W-max (L~ z)) .. z < (N-min (L~ z)) .. z )
set g = Rotate (z,(E-max (L~ z)));
A1: L~ z = L~ (Rotate (z,(E-max (L~ z)))) by REVROT_1:33;
 E-max (L~ z) in rng z by SPRECT_2:46;
then A2: (Rotate (z,(E-max (L~ z)))) /. 1 = E-max (L~ (Rotate (z,(E-max (L~ z))))) by A1, FINSEQ_6:92;
then A3: (E-min (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) < (W-max (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) by Lm29;
assume that
A4: z /. 1 = E-min (L~ z) and
A5: W-max (L~ z) <> N-min (L~ z) ; ::_thesis: (W-max (L~ z)) .. z < (N-min (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A6: Rotate ((Rotate (z,(E-max (L~ z)))),(E-min (L~ z))) = z by A4, REVROT_1:16;
A7: ( N-min (L~ (Rotate (z,(E-max (L~ z))))) in rng (Rotate (z,(E-max (L~ z)))) & W-max (L~ (Rotate (z,(E-max (L~ z))))) in rng (Rotate (z,(E-max (L~ z)))) ) by SPRECT_2:39, SPRECT_2:44;
 ( E-min (L~ (Rotate (z,(E-max (L~ z))))) in rng (Rotate (z,(E-max (L~ z)))) & (W-max (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) < (N-min (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) ) by A1, A5, A2, Th43, SPRECT_2:45;
hence  (W-max (L~ z)) .. z < (N-min (L~ z)) .. z by A1, A6, A7, A3, Th5; ::_thesis: verum
end;

theorem :: SPRECT_5:57
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = E-min (L~ z) implies (N-min (L~ z)) .. z < (N-max (L~ z)) .. z )
set g = Rotate (z,(W-min (L~ z)));
A1: L~ z = L~ (Rotate (z,(W-min (L~ z)))) by REVROT_1:33;
 W-min (L~ z) in rng z by SPRECT_2:43;
then  (Rotate (z,(W-min (L~ z)))) /. 1 = W-min (L~ (Rotate (z,(W-min (L~ z))))) by A1, FINSEQ_6:92;
then A2: ( (N-min (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) < (N-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) & (N-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) < (E-min (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) ) by Lm16, Th24;
A3: E-min (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) by SPRECT_2:45;
assume A4: z /. 1 = E-min (L~ z) ; ::_thesis: (N-min (L~ z)) .. z < (N-max (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A5: Rotate ((Rotate (z,(W-min (L~ z)))),(E-min (L~ z))) = z by A4, REVROT_1:16;
 ( N-min (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) & N-max (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) ) by SPRECT_2:39, SPRECT_2:40;
hence  (N-min (L~ z)) .. z < (N-max (L~ z)) .. z by A1, A5, A3, A2, Th11; ::_thesis: verum
end;

theorem :: SPRECT_5:58
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = E-min (L~ z) & E-max (L~ z) <> N-max (L~ z) implies (N-max (L~ z)) .. z < (E-max (L~ z)) .. z )
set g = Rotate (z,(W-min (L~ z)));
A1: L~ z = L~ (Rotate (z,(W-min (L~ z)))) by REVROT_1:33;
 W-min (L~ z) in rng z by SPRECT_2:43;
then A2: (Rotate (z,(W-min (L~ z)))) /. 1 = W-min (L~ (Rotate (z,(W-min (L~ z))))) by A1, FINSEQ_6:92;
then A3: (E-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) < (E-min (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) by Th26;
assume that
A4: z /. 1 = E-min (L~ z) and
A5: E-max (L~ z) <> N-max (L~ z) ; ::_thesis: (N-max (L~ z)) .. z < (E-max (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A6: Rotate ((Rotate (z,(W-min (L~ z)))),(E-min (L~ z))) = z by A4, REVROT_1:16;
A7: ( E-max (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) & N-max (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) ) by SPRECT_2:40, SPRECT_2:46;
 ( E-min (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) & (N-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) < (E-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) ) by A1, A5, A2, Th25, SPRECT_2:45;
hence  (N-max (L~ z)) .. z < (E-max (L~ z)) .. z by A1, A6, A7, A3, Th11; ::_thesis: verum
end;

theorem :: SPRECT_5:59
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
let f be non constant standard special_circular_sequence; ::_thesis: ( f /. 1 = S-min (L~ f) & S-min (L~ f) <> W-min (L~ f) implies (S-min (L~ f)) .. f < (W-min (L~ f)) .. f )
assume that
A1: f /. 1 = S-min (L~ f) and
A2: S-min (L~ f) <> W-min (L~ f) ; ::_thesis: (S-min (L~ f)) .. f < (W-min (L~ f)) .. f
A3: W-min (L~ f) in rng f by SPRECT_2:43;
then  (W-min (L~ f)) .. f in dom f by FINSEQ_4:20;
then A4: (W-min (L~ f)) .. f >= 1 by FINSEQ_3:25;
 ( S-min (L~ f) in rng f & (S-min (L~ f)) .. f = 1 ) by A1, FINSEQ_6:43, SPRECT_2:41;
hence  (S-min (L~ f)) .. f < (W-min (L~ f)) .. f by A3, A2, A4, FINSEQ_5:9, XXREAL_0:1; ::_thesis: verum
end;

theorem :: SPRECT_5:60
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = S-min (L~ z) implies (W-min (L~ z)) .. z < (W-max (L~ z)) .. z )
set g = Rotate (z,(E-max (L~ z)));
A1: L~ z = L~ (Rotate (z,(E-max (L~ z)))) by REVROT_1:33;
 E-max (L~ z) in rng z by SPRECT_2:46;
then  (Rotate (z,(E-max (L~ z)))) /. 1 = E-max (L~ (Rotate (z,(E-max (L~ z))))) by A1, FINSEQ_6:92;
then A2: ( (S-min (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) <= (W-min (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) & (W-min (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) < (W-max (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) ) by Th41, Th42;
A3: W-min (L~ (Rotate (z,(E-max (L~ z))))) in rng (Rotate (z,(E-max (L~ z)))) by SPRECT_2:43;
assume A4: z /. 1 = S-min (L~ z) ; ::_thesis: (W-min (L~ z)) .. z < (W-max (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A5: Rotate ((Rotate (z,(E-max (L~ z)))),(S-min (L~ z))) = z by A4, REVROT_1:16;
 ( W-max (L~ (Rotate (z,(E-max (L~ z))))) in rng (Rotate (z,(E-max (L~ z)))) & S-min (L~ (Rotate (z,(E-max (L~ z))))) in rng (Rotate (z,(E-max (L~ z)))) ) by SPRECT_2:41, SPRECT_2:44;
hence  (W-min (L~ z)) .. z < (W-max (L~ z)) .. z by A1, A5, A3, A2, Th5; ::_thesis: verum
end;

theorem :: SPRECT_5:61
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = S-min (L~ z) & W-max (L~ z) <> N-min (L~ z) implies (W-max (L~ z)) .. z < (N-min (L~ z)) .. z )
set g = Rotate (z,(E-max (L~ z)));
A1: L~ z = L~ (Rotate (z,(E-max (L~ z)))) by REVROT_1:33;
 E-max (L~ z) in rng z by SPRECT_2:46;
then A2: (Rotate (z,(E-max (L~ z)))) /. 1 = E-max (L~ (Rotate (z,(E-max (L~ z))))) by A1, FINSEQ_6:92;
then A3: ( N-min (L~ (Rotate (z,(E-max (L~ z))))) in rng (Rotate (z,(E-max (L~ z)))) & (S-min (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) < (W-max (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) ) by Lm30, SPRECT_2:39;
assume that
A4: z /. 1 = S-min (L~ z) and
A5: W-max (L~ z) <> N-min (L~ z) ; ::_thesis: (W-max (L~ z)) .. z < (N-min (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A6: Rotate ((Rotate (z,(E-max (L~ z)))),(S-min (L~ z))) = z by A4, REVROT_1:16;
A7: ( W-max (L~ (Rotate (z,(E-max (L~ z))))) in rng (Rotate (z,(E-max (L~ z)))) & S-min (L~ (Rotate (z,(E-max (L~ z))))) in rng (Rotate (z,(E-max (L~ z)))) ) by SPRECT_2:41, SPRECT_2:44;
 (W-max (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) < (N-min (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) by A1, A5, A2, Th43;
hence  (W-max (L~ z)) .. z < (N-min (L~ z)) .. z by A1, A6, A7, A3, Th5; ::_thesis: verum
end;

theorem :: SPRECT_5:62
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = S-min (L~ z) implies (N-min (L~ z)) .. z < (N-max (L~ z)) .. z )
set g = Rotate (z,(S-max (L~ z)));
A1: L~ z = L~ (Rotate (z,(S-max (L~ z)))) by REVROT_1:33;
 S-max (L~ z) in rng z by SPRECT_2:42;
then  (Rotate (z,(S-max (L~ z)))) /. 1 = S-max (L~ (Rotate (z,(S-max (L~ z))))) by A1, FINSEQ_6:92;
then A2: ( (N-min (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) < (N-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) & (S-min (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) < (N-min (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) ) by Lm25, Th34;
A3: S-min (L~ (Rotate (z,(S-max (L~ z))))) in rng (Rotate (z,(S-max (L~ z)))) by SPRECT_2:41;
assume A4: z /. 1 = S-min (L~ z) ; ::_thesis: (N-min (L~ z)) .. z < (N-max (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A5: Rotate ((Rotate (z,(S-max (L~ z)))),(S-min (L~ z))) = z by A4, REVROT_1:16;
 ( N-min (L~ (Rotate (z,(S-max (L~ z))))) in rng (Rotate (z,(S-max (L~ z)))) & N-max (L~ (Rotate (z,(S-max (L~ z))))) in rng (Rotate (z,(S-max (L~ z)))) ) by SPRECT_2:39, SPRECT_2:40;
hence  (N-min (L~ z)) .. z < (N-max (L~ z)) .. z by A1, A5, A3, A2, Th5; ::_thesis: verum
end;

theorem :: SPRECT_5:63
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = S-min (L~ z) & N-max (L~ z) <> E-max (L~ z) implies (N-max (L~ z)) .. z < (E-max (L~ z)) .. z )
set g = Rotate (z,(S-max (L~ z)));
A1: L~ z = L~ (Rotate (z,(S-max (L~ z)))) by REVROT_1:33;
 S-max (L~ z) in rng z by SPRECT_2:42;
then A2: (Rotate (z,(S-max (L~ z)))) /. 1 = S-max (L~ (Rotate (z,(S-max (L~ z))))) by A1, FINSEQ_6:92;
then A3: (S-min (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) < (N-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) by Lm26;
assume that
A4: z /. 1 = S-min (L~ z) and
A5: N-max (L~ z) <> E-max (L~ z) ; ::_thesis: (N-max (L~ z)) .. z < (E-max (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A6: Rotate ((Rotate (z,(S-max (L~ z)))),(S-min (L~ z))) = z by A4, REVROT_1:16;
A7: ( E-max (L~ (Rotate (z,(S-max (L~ z))))) in rng (Rotate (z,(S-max (L~ z)))) & N-max (L~ (Rotate (z,(S-max (L~ z))))) in rng (Rotate (z,(S-max (L~ z)))) ) by SPRECT_2:40, SPRECT_2:46;
 ( S-min (L~ (Rotate (z,(S-max (L~ z))))) in rng (Rotate (z,(S-max (L~ z)))) & (N-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) < (E-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) ) by A1, A5, A2, Th35, SPRECT_2:41;
hence  (N-max (L~ z)) .. z < (E-max (L~ z)) .. z by A1, A6, A7, A3, Th5; ::_thesis: verum
end;

theorem :: SPRECT_5:64
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = S-min (L~ z) implies (E-max (L~ z)) .. z < (E-min (L~ z)) .. z )
set g = Rotate (z,(N-min (L~ z)));
A1: L~ z = L~ (Rotate (z,(N-min (L~ z)))) by REVROT_1:33;
 N-min (L~ z) in rng z by SPRECT_2:39;
then  (Rotate (z,(N-min (L~ z)))) /. 1 = N-min (L~ (Rotate (z,(N-min (L~ z))))) by A1, FINSEQ_6:92;
then A2: ( (E-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) < (E-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) & (E-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) < (S-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) ) by Lm4, SPRECT_2:71;
A3: S-min (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) by SPRECT_2:41;
assume A4: z /. 1 = S-min (L~ z) ; ::_thesis: (E-max (L~ z)) .. z < (E-min (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A5: Rotate ((Rotate (z,(N-min (L~ z)))),(S-min (L~ z))) = z by A4, REVROT_1:16;
 ( E-max (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) & E-min (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) ) by SPRECT_2:45, SPRECT_2:46;
hence  (E-max (L~ z)) .. z < (E-min (L~ z)) .. z by A1, A5, A3, A2, Th11; ::_thesis: verum
end;

theorem :: SPRECT_5:65
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = S-min (L~ z) & S-max (L~ z) <> E-min (L~ z) implies (E-min (L~ z)) .. z < (S-max (L~ z)) .. z )
set g = Rotate (z,(N-min (L~ z)));
A1: L~ z = L~ (Rotate (z,(N-min (L~ z)))) by REVROT_1:33;
 N-min (L~ z) in rng z by SPRECT_2:39;
then A2: (Rotate (z,(N-min (L~ z)))) /. 1 = N-min (L~ (Rotate (z,(N-min (L~ z))))) by A1, FINSEQ_6:92;
then A3: (S-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) < (S-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) by SPRECT_2:73;
assume that
A4: z /. 1 = S-min (L~ z) and
A5: S-max (L~ z) <> E-min (L~ z) ; ::_thesis: (E-min (L~ z)) .. z < (S-max (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A6: Rotate ((Rotate (z,(N-min (L~ z)))),(S-min (L~ z))) = z by A4, REVROT_1:16;
A7: ( S-max (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) & E-min (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) ) by SPRECT_2:42, SPRECT_2:45;
 ( S-min (L~ (Rotate (z,(N-min (L~ z))))) in rng (Rotate (z,(N-min (L~ z)))) & (E-min (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) < (S-max (L~ (Rotate (z,(N-min (L~ z)))))) .. (Rotate (z,(N-min (L~ z)))) ) by A1, A5, A2, SPRECT_2:41, SPRECT_2:72;
hence  (E-min (L~ z)) .. z < (S-max (L~ z)) .. z by A1, A6, A7, A3, Th11; ::_thesis: verum
end;

theorem :: SPRECT_5:66
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
let f be non constant standard special_circular_sequence; ::_thesis: ( f /. 1 = W-max (L~ f) & W-max (L~ f) <> N-min (L~ f) implies (W-max (L~ f)) .. f < (N-min (L~ f)) .. f )
assume that
A1: f /. 1 = W-max (L~ f) and
A2: W-max (L~ f) <> N-min (L~ f) ; ::_thesis: (W-max (L~ f)) .. f < (N-min (L~ f)) .. f
A3: N-min (L~ f) in rng f by SPRECT_2:39;
then  (N-min (L~ f)) .. f in dom f by FINSEQ_4:20;
then A4: (N-min (L~ f)) .. f >= 1 by FINSEQ_3:25;
 ( W-max (L~ f) in rng f & (W-max (L~ f)) .. f = 1 ) by A1, FINSEQ_6:43, SPRECT_2:44;
hence  (W-max (L~ f)) .. f < (N-min (L~ f)) .. f by A3, A2, A4, FINSEQ_5:9, XXREAL_0:1; ::_thesis: verum
end;

theorem :: SPRECT_5:67
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = W-max (L~ z) implies (N-min (L~ z)) .. z < (N-max (L~ z)) .. z )
set g = Rotate (z,(S-max (L~ z)));
A1: L~ z = L~ (Rotate (z,(S-max (L~ z)))) by REVROT_1:33;
 S-max (L~ z) in rng z by SPRECT_2:42;
then  (Rotate (z,(S-max (L~ z)))) /. 1 = S-max (L~ (Rotate (z,(S-max (L~ z))))) by A1, FINSEQ_6:92;
then A2: ( (W-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) <= (N-min (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) & (N-min (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) < (N-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) ) by Th33, Th34;
A3: N-min (L~ (Rotate (z,(S-max (L~ z))))) in rng (Rotate (z,(S-max (L~ z)))) by SPRECT_2:39;
assume A4: z /. 1 = W-max (L~ z) ; ::_thesis: (N-min (L~ z)) .. z < (N-max (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A5: Rotate ((Rotate (z,(S-max (L~ z)))),(W-max (L~ z))) = z by A4, REVROT_1:16;
 ( N-max (L~ (Rotate (z,(S-max (L~ z))))) in rng (Rotate (z,(S-max (L~ z)))) & W-max (L~ (Rotate (z,(S-max (L~ z))))) in rng (Rotate (z,(S-max (L~ z)))) ) by SPRECT_2:40, SPRECT_2:44;
hence  (N-min (L~ z)) .. z < (N-max (L~ z)) .. z by A1, A5, A3, A2, Th5; ::_thesis: verum
end;

theorem :: SPRECT_5:68
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = W-max (L~ z) & N-max (L~ z) <> E-max (L~ z) implies (N-max (L~ z)) .. z < (E-max (L~ z)) .. z )
set g = Rotate (z,(S-max (L~ z)));
A1: L~ z = L~ (Rotate (z,(S-max (L~ z)))) by REVROT_1:33;
 S-max (L~ z) in rng z by SPRECT_2:42;
then A2: (Rotate (z,(S-max (L~ z)))) /. 1 = S-max (L~ (Rotate (z,(S-max (L~ z))))) by A1, FINSEQ_6:92;
then A3: ( E-max (L~ (Rotate (z,(S-max (L~ z))))) in rng (Rotate (z,(S-max (L~ z)))) & (W-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) < (N-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) ) by Lm23, SPRECT_2:46;
assume that
A4: z /. 1 = W-max (L~ z) and
A5: N-max (L~ z) <> E-max (L~ z) ; ::_thesis: (N-max (L~ z)) .. z < (E-max (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A6: Rotate ((Rotate (z,(S-max (L~ z)))),(W-max (L~ z))) = z by A4, REVROT_1:16;
A7: ( N-max (L~ (Rotate (z,(S-max (L~ z))))) in rng (Rotate (z,(S-max (L~ z)))) & W-max (L~ (Rotate (z,(S-max (L~ z))))) in rng (Rotate (z,(S-max (L~ z)))) ) by SPRECT_2:40, SPRECT_2:44;
 (N-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) < (E-max (L~ (Rotate (z,(S-max (L~ z)))))) .. (Rotate (z,(S-max (L~ z)))) by A1, A5, A2, Th35;
hence  (N-max (L~ z)) .. z < (E-max (L~ z)) .. z by A1, A6, A7, A3, Th5; ::_thesis: verum
end;

theorem :: SPRECT_5:69
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = W-max (L~ z) implies (E-max (L~ z)) .. z < (E-min (L~ z)) .. z )
set g = Rotate (z,(W-min (L~ z)));
A1: L~ z = L~ (Rotate (z,(W-min (L~ z)))) by REVROT_1:33;
 W-min (L~ z) in rng z by SPRECT_2:43;
then  (Rotate (z,(W-min (L~ z)))) /. 1 = W-min (L~ (Rotate (z,(W-min (L~ z))))) by A1, FINSEQ_6:92;
then A2: ( (E-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) < (E-min (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) & (W-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) < (E-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) ) by Lm18, Th26;
A3: W-max (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) by SPRECT_2:44;
assume A4: z /. 1 = W-max (L~ z) ; ::_thesis: (E-max (L~ z)) .. z < (E-min (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A5: Rotate ((Rotate (z,(W-min (L~ z)))),(W-max (L~ z))) = z by A4, REVROT_1:16;
 ( E-max (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) & E-min (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) ) by SPRECT_2:45, SPRECT_2:46;
hence  (E-max (L~ z)) .. z < (E-min (L~ z)) .. z by A1, A5, A3, A2, Th5; ::_thesis: verum
end;

theorem :: SPRECT_5:70
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = W-max (L~ z) & E-min (L~ z) <> S-max (L~ z) implies (E-min (L~ z)) .. z < (S-max (L~ z)) .. z )
set g = Rotate (z,(W-min (L~ z)));
A1: L~ z = L~ (Rotate (z,(W-min (L~ z)))) by REVROT_1:33;
 W-min (L~ z) in rng z by SPRECT_2:43;
then A2: (Rotate (z,(W-min (L~ z)))) /. 1 = W-min (L~ (Rotate (z,(W-min (L~ z))))) by A1, FINSEQ_6:92;
then A3: (W-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) < (E-min (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) by Lm19;
assume that
A4: z /. 1 = W-max (L~ z) and
A5: E-min (L~ z) <> S-max (L~ z) ; ::_thesis: (E-min (L~ z)) .. z < (S-max (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A6: Rotate ((Rotate (z,(W-min (L~ z)))),(W-max (L~ z))) = z by A4, REVROT_1:16;
A7: ( S-max (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) & E-min (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) ) by SPRECT_2:42, SPRECT_2:45;
 ( W-max (L~ (Rotate (z,(W-min (L~ z))))) in rng (Rotate (z,(W-min (L~ z)))) & (E-min (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) < (S-max (L~ (Rotate (z,(W-min (L~ z)))))) .. (Rotate (z,(W-min (L~ z)))) ) by A1, A5, A2, Th27, SPRECT_2:44;
hence  (E-min (L~ z)) .. z < (S-max (L~ z)) .. z by A1, A6, A7, A3, Th5; ::_thesis: verum
end;

theorem :: SPRECT_5:71
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = W-max (L~ z) implies (S-max (L~ z)) .. z < (S-min (L~ z)) .. z )
set g = Rotate (z,(E-max (L~ z)));
A1: L~ z = L~ (Rotate (z,(E-max (L~ z)))) by REVROT_1:33;
 E-max (L~ z) in rng z by SPRECT_2:46;
then  (Rotate (z,(E-max (L~ z)))) /. 1 = E-max (L~ (Rotate (z,(E-max (L~ z))))) by A1, FINSEQ_6:92;
then A2: ( (S-max (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) < (S-min (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) & (S-min (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) < (W-max (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) ) by Lm30, Th40;
A3: W-max (L~ (Rotate (z,(E-max (L~ z))))) in rng (Rotate (z,(E-max (L~ z)))) by SPRECT_2:44;
assume A4: z /. 1 = W-max (L~ z) ; ::_thesis: (S-max (L~ z)) .. z < (S-min (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A5: Rotate ((Rotate (z,(E-max (L~ z)))),(W-max (L~ z))) = z by A4, REVROT_1:16;
 ( S-max (L~ (Rotate (z,(E-max (L~ z))))) in rng (Rotate (z,(E-max (L~ z)))) & S-min (L~ (Rotate (z,(E-max (L~ z))))) in rng (Rotate (z,(E-max (L~ z)))) ) by SPRECT_2:41, SPRECT_2:42;
hence  (S-max (L~ z)) .. z < (S-min (L~ z)) .. z by A1, A5, A3, A2, Th11; ::_thesis: verum
end;

theorem :: SPRECT_5:72
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
let z be non constant standard clockwise_oriented special_circular_sequence; ::_thesis: ( z /. 1 = W-max (L~ z) & W-min (L~ z) <> S-min (L~ z) implies (S-min (L~ z)) .. z < (W-min (L~ z)) .. z )
set g = Rotate (z,(E-max (L~ z)));
A1: L~ z = L~ (Rotate (z,(E-max (L~ z)))) by REVROT_1:33;
 E-max (L~ z) in rng z by SPRECT_2:46;
then A2: (Rotate (z,(E-max (L~ z)))) /. 1 = E-max (L~ (Rotate (z,(E-max (L~ z))))) by A1, FINSEQ_6:92;
then A3: (W-min (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) < (W-max (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) by Th42;
assume that
A4: z /. 1 = W-max (L~ z) and
A5: W-min (L~ z) <> S-min (L~ z) ; ::_thesis: (S-min (L~ z)) .. z < (W-min (L~ z)) .. z
 for i being Element of NAT st 1 < i & i < len z holds
z /. i <> z /. 1 by GOBOARD7:36;
then A6: Rotate ((Rotate (z,(E-max (L~ z)))),(W-max (L~ z))) = z by A4, REVROT_1:16;
A7: ( W-min (L~ (Rotate (z,(E-max (L~ z))))) in rng (Rotate (z,(E-max (L~ z)))) & S-min (L~ (Rotate (z,(E-max (L~ z))))) in rng (Rotate (z,(E-max (L~ z)))) ) by SPRECT_2:41, SPRECT_2:43;
 ( W-max (L~ (Rotate (z,(E-max (L~ z))))) in rng (Rotate (z,(E-max (L~ z)))) & (S-min (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) < (W-min (L~ (Rotate (z,(E-max (L~ z)))))) .. (Rotate (z,(E-max (L~ z)))) ) by A1, A5, A2, Th41, SPRECT_2:44;
hence  (S-min (L~ z)) .. z < (W-min (L~ z)) .. z by A1, A6, A7, A3, Th11; ::_thesis: verum
end;