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