sprect_5.miz



    begin

    reserve D for non empty set,

f for FinSequence of D,

g for circular FinSequence of D,

p,p1,p2,p3,q for Element of D;

    theorem :: SPRECT_5:1

    

     Th1: q in ( rng (f | (p .. f))) implies (q .. f) <= (p .. f)

    proof

      assume

       A1: q in ( rng (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 thesis by A2, XXREAL_0: 2;

    end;

    theorem :: SPRECT_5:2

    

     Th2: p in ( rng f) & q in ( rng f) & (p .. f) <= (q .. f) implies (q .. (f :- p)) = (((q .. f) - (p .. f)) + 1)

    proof

      assume that

       A1: p in ( rng f) and

       A2: q in ( rng f) and

       A3: (p .. f) <= (q .. f);

      

       A4: f = ((f | (p .. f)) ^ (f /^ (p .. f))) by RFINSEQ: 8;

      per cases by A3, XXREAL_0: 1;

        suppose (p .. f) = (q .. f);

        then p = q by A1, A2, FINSEQ_5: 9;

        hence thesis by FINSEQ_6: 79;

      end;

        suppose

         A5: (p .. f) < (q .. f);

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

      end;

    end;

    theorem :: SPRECT_5:3

    

     Th3: p in ( rng f) & q in ( rng f) & (p .. f) <= (q .. f) implies (p .. (f -: q)) = (p .. f)

    proof

      

       A1: (f -: q) = (f | (q .. f)) by FINSEQ_5:def 1;

      assume p in ( rng f) & q in ( rng f) & (p .. f) <= (q .. f);

      then p in ( rng (f | (q .. f))) by A1, FINSEQ_5: 46;

      hence thesis by A1, FINSEQ_5: 40;

    end;

    theorem :: SPRECT_5:4

    

     Th4: p in ( rng f) & q in ( rng f) & (p .. f) <= (q .. f) implies (q .. ( Rotate (f,p))) = (((q .. f) - (p .. f)) + 1)

    proof

      assume that

       A1: p in ( rng f) and

       A2: q in ( rng f);

      

       A3: ( Rotate (f,p)) = ((f :- p) ^ ((f -: p) /^ 1)) by A1, FINSEQ_6:def 2;

      assume

       A4: (p .. f) <= (q .. f);

      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;

    end;

    theorem :: SPRECT_5:5

    

     Th5: 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)))

    proof

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

      

       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 thesis by A3, XREAL_1: 6;

    end;

    theorem :: SPRECT_5:6

    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)))

    proof

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

      per cases by A4, XXREAL_0: 1;

        suppose (p2 .. f) < (p3 .. f);

        hence thesis by A1, A2, A3, Th5;

      end;

        suppose (p2 .. f) = (p3 .. f);

        hence thesis by A2, FINSEQ_5: 9;

      end;

    end;

    theorem :: SPRECT_5:7

    

     Th7: p in ( rng g) & ( len g) > 1 implies (p .. g) < ( len g)

    proof

      assume that

       A1: p in ( rng g) and

       A2: ( len g) > 1 and

       A3: (p .. g) >= ( len g);

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

      g is non empty by A2, CARD_1: 27;

      hence contradiction by A2, A3, A4, FINSEQ_6: 43;

    end;

    begin

    reserve f for non constant standard special_circular_sequence,

p,p1,p2,p3,q for Point of ( TOP-REAL 2);

    registration

      let f;

      cluster (f /^ 1) -> one-to-one;

      coherence

      proof

        let x1,x2 be object such that

         A1: x1 in ( dom (f /^ 1)) and

         A2: x2 in ( dom (f /^ 1)) and

         A3: ((f /^ 1) . x1) = ((f /^ 1) . x2);

        reconsider i = x1, j = x2 as 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;

        per cases by A8, XXREAL_0: 1;

          suppose i < j;

          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;

        end;

          suppose j < i;

          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;

        end;

      end;

    end

    theorem :: SPRECT_5:8

    

     Th8: 1 < (q .. f) & q in ( rng f) implies ((f /. 1) .. ( Rotate (f,q))) = ((( len f) + 1) - (q .. f))

    proof

      assume that

       A1: 1 < (q .. f) and

       A2: q in ( rng 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: i = ((1 + ( len f)) - (q .. f)) by XREAL_1: 233;

      then (i + ((q .. f) - 1)) = ( len f);

      then i < ( len f) by A3, XREAL_1: 29;

      then

       A7: i < ( len ( Rotate (f,q))) by FINSEQ_6: 179;

      now

        assume ((q .. f) + 0 ) >= ( len f);

        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;

      end;

      then

       A9: (( len f) - (q .. f)) > 0 by XREAL_1: 20;

      i = (1 + (( len f) - (q .. f))) by A6;

      then

       A10: (1 + 0 ) < i by A9, XREAL_1: 6;

      then

       A11: i in ( dom ( Rotate (f,q))) by A7, FINSEQ_3: 25;

      

       A12: (f /. 1) = (( Rotate (f,q)) /. ((1 + ( len f)) -' (q .. f))) by A1, A2, FINSEQ_6: 183;

      then

       A13: (f /. 1) = (( Rotate (f,q)) . i) by A11, PARTFUN1:def 6;

      for j be object st j in ( dom ( Rotate (f,q))) & j <> i holds (( Rotate (f,q)) . j) <> (f /. 1)

      proof

        let z be object;

        assume that

         A14: z in ( dom ( Rotate (f,q))) and

         A15: z <> i;

        reconsider j = z as Nat by A14;

        per cases by A15, XXREAL_0: 1;

          suppose

           A16: j < i;

          1 <= j by A14, FINSEQ_3: 25;

          then (( Rotate (f,q)) /. j) <> (f /. 1) by A12, A7, A16, GOBOARD7: 36;

          hence thesis by A14, PARTFUN1:def 6;

        end;

          suppose

           A17: i < j;

          j <= ( len ( Rotate (f,q))) by A14, FINSEQ_3: 25;

          then (( Rotate (f,q)) /. j) <> (f /. 1) by A12, A10, A17, GOBOARD7: 37;

          hence thesis by A14, PARTFUN1:def 6;

        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;

    end;

    theorem :: SPRECT_5:9

    

     Th9: p in ( rng f) & q in ( rng f) & (p .. f) < (q .. f) implies (p .. ( Rotate (f,q))) = ((( len f) + (p .. f)) - (q .. f))

    proof

      assume that

       A1: p in ( rng f) and

       A2: q in ( rng f);

      assume

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

      per cases by A6, A4, XXREAL_0: 1;

        suppose

         A8: (p .. f) = 1;

        then p = (f /. 1) by A1, FINSEQ_5: 38;

        hence thesis by A2, A3, A8, Th8;

      end;

        suppose

         A9: (p .. f) > 1;

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

      end;

    end;

    theorem :: SPRECT_5:10

    

     Th10: 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)))

    proof

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

      

       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 thesis by A4, A5, A6, FINSEQ_5: 9, XXREAL_0: 1;

    end;

    theorem :: SPRECT_5:11

    

     Th11: 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)))

    proof

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

      (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 thesis by A5, XREAL_1: 9;

    end;

    theorem :: SPRECT_5:12

    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)))

    proof

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

      per cases by A3, XXREAL_0: 1;

        suppose (p1 .. f) < (p2 .. f);

        hence thesis by A1, A2, A4, Th11;

      end;

        suppose (p1 .. f) = (p2 .. f);

        hence thesis by A1, FINSEQ_5: 9;

      end;

    end;

    theorem :: SPRECT_5:13

    (( S-min ( L~ f)) .. f) < ( len f)

    proof

      ( S-min ( L~ f)) in ( rng f) & ( len f) > 1 by GOBOARD7: 34, SPRECT_2: 41, XXREAL_0: 2;

      hence thesis by Th7;

    end;

    theorem :: SPRECT_5:14

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

    proof

      ( S-max ( L~ f)) in ( rng f) & ( len f) > 1 by GOBOARD7: 34, SPRECT_2: 42, XXREAL_0: 2;

      hence thesis by Th7;

    end;

    theorem :: SPRECT_5:15

    (( E-min ( L~ f)) .. f) < ( len f)

    proof

      ( E-min ( L~ f)) in ( rng f) & ( len f) > 1 by GOBOARD7: 34, SPRECT_2: 45, XXREAL_0: 2;

      hence thesis by Th7;

    end;

    theorem :: SPRECT_5:16

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

    proof

      ( E-max ( L~ f)) in ( rng f) & ( len f) > 1 by GOBOARD7: 34, SPRECT_2: 46, XXREAL_0: 2;

      hence thesis by Th7;

    end;

    theorem :: SPRECT_5:17

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

    proof

      ( N-min ( L~ f)) in ( rng f) & ( len f) > 1 by GOBOARD7: 34, SPRECT_2: 39, XXREAL_0: 2;

      hence thesis by Th7;

    end;

    theorem :: SPRECT_5:18

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

    proof

      ( N-max ( L~ f)) in ( rng f) & ( len f) > 1 by GOBOARD7: 34, SPRECT_2: 40, XXREAL_0: 2;

      hence thesis by Th7;

    end;

    theorem :: SPRECT_5:19

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

    proof

      ( W-max ( L~ f)) in ( rng f) & ( len f) > 1 by GOBOARD7: 34, SPRECT_2: 44, XXREAL_0: 2;

      hence thesis by Th7;

    end;

    theorem :: SPRECT_5:20

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

    proof

      ( W-min ( L~ f)) in ( rng f) & ( len f) > 1 by GOBOARD7: 34, SPRECT_2: 43, XXREAL_0: 2;

      hence thesis by Th7;

    end;

    begin

    reserve z for clockwise_oriented non constant standard special_circular_sequence;

    

     Lm1: (z /. 1) = ( N-min ( L~ z)) implies (( E-max ( L~ z)) .. z) < (( S-max ( L~ z)) .. z)

    proof

      assume

       A1: (z /. 1) = ( N-min ( L~ z));

      then (( E-max ( L~ z)) .. z) < (( E-min ( L~ z)) .. z) by SPRECT_2: 71;

      hence thesis by A1, SPRECT_2: 72, XXREAL_0: 2;

    end;

    

     Lm2: (z /. 1) = ( N-min ( L~ z)) implies (( E-max ( L~ z)) .. z) < (( S-min ( L~ z)) .. z)

    proof

      assume

       A1: (z /. 1) = ( N-min ( L~ z));

      then (( E-max ( L~ z)) .. z) < (( S-max ( L~ z)) .. z) by Lm1;

      hence thesis by A1, SPRECT_2: 73, XXREAL_0: 2;

    end;

    

     Lm3: (z /. 1) = ( N-min ( L~ z)) implies (( E-max ( L~ z)) .. z) < (( W-min ( L~ z)) .. z)

    proof

      assume

       A1: (z /. 1) = ( N-min ( L~ z));

      then (( E-max ( L~ z)) .. z) < (( S-min ( L~ z)) .. z) by Lm2;

      hence thesis by A1, SPRECT_2: 74, XXREAL_0: 2;

    end;

    

     Lm4: (z /. 1) = ( N-min ( L~ z)) implies (( E-min ( L~ z)) .. z) < (( S-min ( L~ z)) .. z)

    proof

      assume

       A1: (z /. 1) = ( N-min ( L~ z));

      then (( S-max ( L~ z)) .. z) < (( S-min ( L~ z)) .. z) by SPRECT_2: 73;

      hence thesis by A1, SPRECT_2: 72, XXREAL_0: 2;

    end;

    

     Lm5: (z /. 1) = ( N-min ( L~ z)) implies (( E-min ( L~ z)) .. z) < (( W-min ( L~ z)) .. z)

    proof

      assume

       A1: (z /. 1) = ( N-min ( L~ z));

      then (( E-min ( L~ z)) .. z) < (( S-min ( L~ z)) .. z) by Lm4;

      hence thesis by A1, SPRECT_2: 74, XXREAL_0: 2;

    end;

    

     Lm6: (z /. 1) = ( N-min ( L~ z)) implies (( S-max ( L~ z)) .. z) < (( W-min ( L~ z)) .. z)

    proof

      assume

       A1: (z /. 1) = ( N-min ( L~ z));

      then (( S-max ( L~ z)) .. z) < (( S-min ( L~ z)) .. z) by SPRECT_2: 73;

      hence thesis by A1, SPRECT_2: 74, XXREAL_0: 2;

    end;

    

     Lm7: (z /. 1) = ( N-min ( L~ z)) implies (( N-max ( L~ z)) .. z) < (( W-min ( L~ z)) .. z)

    proof

      assume

       A1: (z /. 1) = ( N-min ( L~ z));

      then (( E-max ( L~ z)) .. z) < (( W-min ( L~ z)) .. z) by Lm3;

      hence thesis by A1, SPRECT_2: 70, XXREAL_0: 2;

    end;

    

     Lm8: (z /. 1) = ( N-min ( L~ z)) implies (( N-min ( L~ z)) .. z) < (( W-min ( L~ z)) .. z)

    proof

      assume

       A1: (z /. 1) = ( N-min ( L~ z));

      then (( N-max ( L~ z)) .. z) < (( W-min ( L~ z)) .. z) by Lm7;

      hence thesis by A1, SPRECT_2: 68, XXREAL_0: 2;

    end;

    

     Lm9: (z /. 1) = ( N-min ( L~ z)) implies (( N-max ( L~ z)) .. z) < (( S-max ( L~ z)) .. z)

    proof

      assume

       A1: (z /. 1) = ( N-min ( L~ z));

      then (( N-max ( L~ z)) .. z) <= (( E-max ( L~ z)) .. z) by SPRECT_2: 70;

      hence thesis by A1, Lm1, XXREAL_0: 2;

    end;

    

     Lm10: (z /. 1) = ( N-min ( L~ z)) implies (( N-max ( L~ z)) .. z) < (( S-min ( L~ z)) .. z)

    proof

      assume

       A1: (z /. 1) = ( N-min ( L~ z));

      then (( N-max ( L~ z)) .. z) < (( S-max ( L~ z)) .. z) by Lm9;

      hence thesis by A1, SPRECT_2: 73, XXREAL_0: 2;

    end;

    theorem :: SPRECT_5:21

    

     Th21: (f /. 1) = ( W-min ( L~ f)) implies (( W-min ( L~ f)) .. f) < (( W-max ( L~ f)) .. f)

    proof

      assume (f /. 1) = ( W-min ( L~ 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 thesis by A3, A1, XXREAL_0: 1;

    end;

    theorem :: SPRECT_5:22

    (f /. 1) = ( W-min ( L~ f)) implies (( W-max ( L~ f)) .. f) > 1

    proof

      assume

       A1: (f /. 1) = ( W-min ( L~ f));

      then (( W-min ( L~ f)) .. f) = 1 by FINSEQ_6: 43;

      hence thesis by A1, Th21;

    end;

    theorem :: SPRECT_5:23

    

     Th23: (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)

    proof

      set g = ( Rotate (z,( N-min ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( N-min ( L~ z)) in ( rng z) by SPRECT_2: 39;

      then

       A2: (g /. 1) = ( N-min ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A3: (( W-min ( L~ g)) .. g) > (( N-min ( L~ g)) .. g) by Lm8;

      assume that

       A4: (z /. 1) = ( W-min ( L~ z)) and

       A5: ( W-max ( L~ z)) <> ( N-min ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A6: ( Rotate (g,( W-min ( L~ z)))) = z by A4, FINSEQ_6: 181;

      

       A7: ( N-min ( L~ g)) in ( rng g) & ( W-max ( L~ g)) in ( rng g) by SPRECT_2: 39, SPRECT_2: 44;

      ( W-min ( L~ g)) in ( rng g) & (( W-min ( L~ g)) .. g) < (( W-max ( L~ g)) .. g) by A1, A5, A2, SPRECT_2: 43, SPRECT_2: 75;

      hence thesis by A1, A6, A7, A3, Th10;

    end;

    theorem :: SPRECT_5:24

    

     Th24: (z /. 1) = ( W-min ( L~ z)) implies (( N-min ( L~ z)) .. z) < (( N-max ( L~ z)) .. z)

    proof

      set g = ( Rotate (z,( N-min ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( N-min ( L~ z)) in ( rng z) by SPRECT_2: 39;

      then (g /. 1) = ( N-min ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A2: (( N-min ( L~ g)) .. g) < (( N-max ( L~ g)) .. g) & (( N-max ( L~ g)) .. g) < (( W-min ( L~ g)) .. g) by Lm7, SPRECT_2: 68;

      

       A3: ( W-min ( L~ g)) in ( rng g) by SPRECT_2: 43;

      assume

       A4: (z /. 1) = ( W-min ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A5: ( Rotate (g,( W-min ( L~ z)))) = z by A4, FINSEQ_6: 181;

      ( N-min ( L~ g)) in ( rng g) & ( N-max ( L~ g)) in ( rng g) by SPRECT_2: 39, SPRECT_2: 40;

      hence thesis by A1, A5, A3, A2, Th11;

    end;

    theorem :: SPRECT_5:25

    

     Th25: (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)

    proof

      set g = ( Rotate (z,( N-min ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( N-min ( L~ z)) in ( rng z) by SPRECT_2: 39;

      then

       A2: (g /. 1) = ( N-min ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A3: (( E-max ( L~ g)) .. g) < (( W-min ( L~ g)) .. g) by Lm3;

      assume that

       A4: (z /. 1) = ( W-min ( L~ z)) and

       A5: ( N-max ( L~ z)) <> ( E-max ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A6: ( Rotate (g,( W-min ( L~ z)))) = z by A4, FINSEQ_6: 181;

      

       A7: ( N-max ( L~ g)) in ( rng g) & ( E-max ( L~ g)) in ( rng g) by SPRECT_2: 40, SPRECT_2: 46;

      ( W-min ( L~ g)) in ( rng g) & (( N-max ( L~ g)) .. g) < (( E-max ( L~ g)) .. g) by A1, A5, A2, SPRECT_2: 43, SPRECT_2: 70;

      hence thesis by A1, A6, A7, A3, Th11;

    end;

    theorem :: SPRECT_5:26

    

     Th26: (z /. 1) = ( W-min ( L~ z)) implies (( E-max ( L~ z)) .. z) < (( E-min ( L~ z)) .. z)

    proof

      set g = ( Rotate (z,( N-min ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( N-min ( L~ z)) in ( rng z) by SPRECT_2: 39;

      then (g /. 1) = ( N-min ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A2: (( E-max ( L~ g)) .. g) < (( E-min ( L~ g)) .. g) & (( E-min ( L~ g)) .. g) < (( W-min ( L~ g)) .. g) by Lm5, SPRECT_2: 71;

      

       A3: ( W-min ( L~ g)) in ( rng g) by SPRECT_2: 43;

      assume

       A4: (z /. 1) = ( W-min ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A5: ( Rotate (g,( W-min ( L~ z)))) = z by A4, FINSEQ_6: 181;

      ( E-min ( L~ g)) in ( rng g) & ( E-max ( L~ g)) in ( rng g) by SPRECT_2: 45, SPRECT_2: 46;

      hence thesis by A1, A5, A3, A2, Th11;

    end;

    theorem :: SPRECT_5:27

    

     Th27: (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)

    proof

      set g = ( Rotate (z,( N-min ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( N-min ( L~ z)) in ( rng z) by SPRECT_2: 39;

      then

       A2: (g /. 1) = ( N-min ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A3: (( S-max ( L~ g)) .. g) < (( W-min ( L~ g)) .. g) by Lm6;

      assume that

       A4: (z /. 1) = ( W-min ( L~ z)) and

       A5: ( E-min ( L~ z)) <> ( S-max ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A6: ( Rotate (g,( W-min ( L~ z)))) = z by A4, FINSEQ_6: 181;

      

       A7: ( E-min ( L~ g)) in ( rng g) & ( S-max ( L~ g)) in ( rng g) by SPRECT_2: 42, SPRECT_2: 45;

      ( W-min ( L~ g)) in ( rng g) & (( E-min ( L~ g)) .. g) < (( S-max ( L~ g)) .. g) by A1, A5, A2, SPRECT_2: 43, SPRECT_2: 72;

      hence thesis by A1, A6, A7, A3, Th11;

    end;

    theorem :: SPRECT_5:28

    (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)

    proof

      set g = ( Rotate (z,( N-min ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      assume

       A2: (z /. 1) = ( W-min ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A3: ( Rotate (g,( W-min ( L~ z)))) = z by A2, FINSEQ_6: 181;

      

       A4: ( S-min ( L~ g)) in ( rng g) & ( S-max ( L~ g)) in ( rng g) by SPRECT_2: 41, SPRECT_2: 42;

      ( N-min ( L~ z)) in ( rng z) by SPRECT_2: 39;

      then

       A5: (g /. 1) = ( N-min ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A6: ( W-min ( L~ g)) in ( rng g) & (( S-max ( L~ g)) .. g) < (( S-min ( L~ g)) .. g) by SPRECT_2: 43, SPRECT_2: 73;

      assume ( S-min ( L~ z)) <> ( W-min ( L~ z));

      then (( S-min ( L~ g)) .. g) < (( W-min ( L~ g)) .. g) by A1, A5, SPRECT_2: 74;

      hence thesis by A1, A3, A4, A6, Th11;

    end;

    theorem :: SPRECT_5:29

    

     Th29: (f /. 1) = ( S-max ( L~ f)) implies (( S-max ( L~ f)) .. f) < (( S-min ( L~ f)) .. f)

    proof

      assume (f /. 1) = ( S-max ( L~ 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 thesis by A3, A1, XXREAL_0: 1;

    end;

    theorem :: SPRECT_5:30

    (f /. 1) = ( S-max ( L~ f)) implies (( S-min ( L~ f)) .. f) > 1

    proof

      assume

       A1: (f /. 1) = ( S-max ( L~ f));

      then (( S-max ( L~ f)) .. f) = 1 by FINSEQ_6: 43;

      hence thesis by A1, Th29;

    end;

    

     Lm11: (z /. 1) = ( W-min ( L~ z)) implies (( E-max ( L~ z)) .. z) < (( S-max ( L~ z)) .. z)

    proof

      assume

       A1: (z /. 1) = ( W-min ( L~ z));

      then (( E-max ( L~ z)) .. z) < (( E-min ( L~ z)) .. z) by Th26;

      hence thesis by A1, Th27, XXREAL_0: 2;

    end;

    

     Lm12: (z /. 1) = ( W-min ( L~ z)) implies (( N-min ( L~ z)) .. z) < (( E-max ( L~ z)) .. z)

    proof

      assume

       A1: (z /. 1) = ( W-min ( L~ z));

      then (( N-min ( L~ z)) .. z) < (( N-max ( L~ z)) .. z) by Th24;

      hence thesis by A1, Th25, XXREAL_0: 2;

    end;

    

     Lm13: (z /. 1) = ( W-min ( L~ z)) implies (( N-min ( L~ z)) .. z) < (( S-max ( L~ z)) .. z)

    proof

      assume

       A1: (z /. 1) = ( W-min ( L~ z));

      then (( N-min ( L~ z)) .. z) < (( E-max ( L~ z)) .. z) by Lm12;

      hence thesis by A1, Lm11, XXREAL_0: 2;

    end;

    

     Lm14: (z /. 1) = ( W-min ( L~ z)) implies (( N-max ( L~ z)) .. z) < (( S-max ( L~ z)) .. z)

    proof

      assume

       A1: (z /. 1) = ( W-min ( L~ z));

      then (( E-max ( L~ z)) .. z) < (( S-max ( L~ z)) .. z) by Lm11;

      hence thesis by A1, Th25, XXREAL_0: 2;

    end;

    

     Lm15: (z /. 1) = ( W-min ( L~ z)) implies (( W-max ( L~ z)) .. z) < (( S-max ( L~ z)) .. z)

    proof

      assume

       A1: (z /. 1) = ( W-min ( L~ z));

      then (( N-min ( L~ z)) .. z) < (( S-max ( L~ z)) .. z) by Lm13;

      hence thesis by A1, Th23, XXREAL_0: 2;

    end;

    

     Lm16: (z /. 1) = ( W-min ( L~ z)) implies (( N-max ( L~ z)) .. z) < (( E-min ( L~ z)) .. z)

    proof

      assume

       A1: (z /. 1) = ( W-min ( L~ z));

      then (( E-max ( L~ z)) .. z) < (( E-min ( L~ z)) .. z) by Th26;

      hence thesis by A1, Th25, XXREAL_0: 2;

    end;

    

     Lm17: (z /. 1) = ( W-min ( L~ z)) implies (( N-min ( L~ z)) .. z) < (( E-max ( L~ z)) .. z)

    proof

      assume

       A1: (z /. 1) = ( W-min ( L~ z));

      then (( N-min ( L~ z)) .. z) < (( N-max ( L~ z)) .. z) by Th24;

      hence thesis by A1, Th25, XXREAL_0: 2;

    end;

    

     Lm18: (z /. 1) = ( W-min ( L~ z)) implies (( W-max ( L~ z)) .. z) < (( E-max ( L~ z)) .. z)

    proof

      assume

       A1: (z /. 1) = ( W-min ( L~ z));

      then (( W-max ( L~ z)) .. z) <= (( N-min ( L~ z)) .. z) by Th23;

      hence thesis by A1, Lm17, XXREAL_0: 2;

    end;

    

     Lm19: (z /. 1) = ( W-min ( L~ z)) implies (( W-max ( L~ z)) .. z) < (( E-min ( L~ z)) .. z)

    proof

      assume

       A1: (z /. 1) = ( W-min ( L~ z));

      then (( W-max ( L~ z)) .. z) < (( E-max ( L~ z)) .. z) by Lm18;

      hence thesis by A1, Th26, XXREAL_0: 2;

    end;

    theorem :: SPRECT_5:31

    

     Th31: (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)

    proof

      set g = ( Rotate (z,( N-min ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( N-min ( L~ z)) in ( rng z) by SPRECT_2: 39;

      then

       A2: (g /. 1) = ( N-min ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A3: ( S-min ( L~ g)) in ( rng g) & (( S-max ( L~ g)) .. g) < (( S-min ( L~ g)) .. g) 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));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A6: ( Rotate (g,( S-max ( L~ z)))) = z by A4, FINSEQ_6: 181;

      

       A7: ( W-min ( L~ g)) in ( rng g) & ( S-max ( L~ g)) in ( rng g) by SPRECT_2: 42, SPRECT_2: 43;

      (( S-min ( L~ g)) .. g) < (( W-min ( L~ g)) .. g) by A1, A5, A2, SPRECT_2: 74;

      hence thesis by A1, A6, A7, A3, Th5;

    end;

    theorem :: SPRECT_5:32

    

     Th32: (z /. 1) = ( S-max ( L~ z)) implies (( W-min ( L~ z)) .. z) < (( W-max ( L~ z)) .. z)

    proof

      set g = ( Rotate (z,( W-min ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( W-min ( L~ z)) in ( rng z) by SPRECT_2: 43;

      then (g /. 1) = ( W-min ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A2: (( S-max ( L~ g)) .. g) > (( W-max ( L~ g)) .. g) & (( W-min ( L~ g)) .. g) < (( W-max ( L~ g)) .. g) by Lm15, Th21;

      

       A3: ( W-min ( L~ g)) in ( rng g) by SPRECT_2: 43;

      assume

       A4: (z /. 1) = ( S-max ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A5: ( Rotate (g,( S-max ( L~ z)))) = z by A4, FINSEQ_6: 181;

      ( S-max ( L~ g)) in ( rng g) & ( W-max ( L~ g)) in ( rng g) by SPRECT_2: 42, SPRECT_2: 44;

      hence thesis by A1, A5, A3, A2, Th11;

    end;

    theorem :: SPRECT_5:33

    

     Th33: (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)

    proof

      set g = ( Rotate (z,( W-min ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( W-min ( L~ z)) in ( rng z) by SPRECT_2: 43;

      then

       A2: (g /. 1) = ( W-min ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A3: (( N-min ( L~ g)) .. g) < (( S-max ( L~ g)) .. g) by Lm13;

      assume that

       A4: (z /. 1) = ( S-max ( L~ z)) and

       A5: ( W-max ( L~ z)) <> ( N-min ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A6: ( Rotate (g,( S-max ( L~ z)))) = z by A4, FINSEQ_6: 181;

      

       A7: ( W-max ( L~ g)) in ( rng g) & ( N-min ( L~ g)) in ( rng g) by SPRECT_2: 39, SPRECT_2: 44;

      ( S-max ( L~ g)) in ( rng g) & (( W-max ( L~ g)) .. g) < (( N-min ( L~ g)) .. g) by A1, A5, A2, Th23, SPRECT_2: 42;

      hence thesis by A1, A6, A7, A3, Th11;

    end;

    theorem :: SPRECT_5:34

    

     Th34: (z /. 1) = ( S-max ( L~ z)) implies (( N-min ( L~ z)) .. z) < (( N-max ( L~ z)) .. z)

    proof

      set g = ( Rotate (z,( W-min ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( W-min ( L~ z)) in ( rng z) by SPRECT_2: 43;

      then (g /. 1) = ( W-min ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A2: (( N-min ( L~ g)) .. g) < (( N-max ( L~ g)) .. g) & (( N-max ( L~ g)) .. g) < (( S-max ( L~ g)) .. g) by Lm14, Th24;

      

       A3: ( S-max ( L~ g)) in ( rng g) by SPRECT_2: 42;

      assume

       A4: (z /. 1) = ( S-max ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A5: ( Rotate (g,( S-max ( L~ z)))) = z by A4, FINSEQ_6: 181;

      ( N-max ( L~ g)) in ( rng g) & ( N-min ( L~ g)) in ( rng g) by SPRECT_2: 39, SPRECT_2: 40;

      hence thesis by A1, A5, A3, A2, Th11;

    end;

    theorem :: SPRECT_5:35

    

     Th35: (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)

    proof

      set g = ( Rotate (z,( W-min ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( W-min ( L~ z)) in ( rng z) by SPRECT_2: 43;

      then

       A2: (g /. 1) = ( W-min ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A3: (( E-max ( L~ g)) .. g) < (( S-max ( L~ g)) .. g) by Lm11;

      assume that

       A4: (z /. 1) = ( S-max ( L~ z)) and

       A5: ( N-max ( L~ z)) <> ( E-max ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A6: ( Rotate (g,( S-max ( L~ z)))) = z by A4, FINSEQ_6: 181;

      

       A7: ( N-max ( L~ g)) in ( rng g) & ( E-max ( L~ g)) in ( rng g) by SPRECT_2: 40, SPRECT_2: 46;

      ( S-max ( L~ g)) in ( rng g) & (( N-max ( L~ g)) .. g) < (( E-max ( L~ g)) .. g) by A1, A5, A2, Th25, SPRECT_2: 42;

      hence thesis by A1, A6, A7, A3, Th11;

    end;

    theorem :: SPRECT_5:36

    (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)

    proof

      set g = ( Rotate (z,( W-min ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      assume

       A2: (z /. 1) = ( S-max ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A3: ( Rotate (g,( S-max ( L~ z)))) = z by A2, FINSEQ_6: 181;

      

       A4: ( E-min ( L~ g)) in ( rng g) & ( E-max ( L~ g)) in ( rng g) by SPRECT_2: 45, SPRECT_2: 46;

      ( W-min ( L~ z)) in ( rng z) by SPRECT_2: 43;

      then

       A5: (g /. 1) = ( W-min ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A6: ( S-max ( L~ g)) in ( rng g) & (( E-max ( L~ g)) .. g) < (( E-min ( L~ g)) .. g) by Th26, SPRECT_2: 42;

      assume ( E-min ( L~ z)) <> ( S-max ( L~ z));

      then (( E-min ( L~ g)) .. g) < (( S-max ( L~ g)) .. g) by A1, A5, Th27;

      hence thesis by A1, A3, A4, A6, Th11;

    end;

    theorem :: SPRECT_5:37

    

     Th37: (f /. 1) = ( E-max ( L~ f)) implies (( E-max ( L~ f)) .. f) < (( E-min ( L~ f)) .. f)

    proof

      assume (f /. 1) = ( E-max ( L~ 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 thesis by A3, A1, XXREAL_0: 1;

    end;

    theorem :: SPRECT_5:38

    (f /. 1) = ( E-max ( L~ f)) implies (( E-min ( L~ f)) .. f) > 1

    proof

      assume

       A1: (f /. 1) = ( E-max ( L~ f));

      then (( E-max ( L~ f)) .. f) = 1 by FINSEQ_6: 43;

      hence thesis by A1, Th37;

    end;

    theorem :: SPRECT_5:39

    

     Th39: (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)

    proof

      set g = ( Rotate (z,( N-min ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( N-min ( L~ z)) in ( rng z) by SPRECT_2: 39;

      then

       A2: (g /. 1) = ( N-min ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A3: ( E-min ( L~ g)) in ( rng g) & (( E-max ( L~ g)) .. g) < (( E-min ( L~ g)) .. g) 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));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A6: ( Rotate (g,( E-max ( L~ z)))) = z by A4, FINSEQ_6: 181;

      

       A7: ( S-max ( L~ g)) in ( rng g) & ( E-max ( L~ g)) in ( rng g) by SPRECT_2: 42, SPRECT_2: 46;

      (( E-min ( L~ g)) .. g) < (( S-max ( L~ g)) .. g) by A1, A5, A2, SPRECT_2: 72;

      hence thesis by A1, A6, A7, A3, Th5;

    end;

    theorem :: SPRECT_5:40

    

     Th40: (z /. 1) = ( E-max ( L~ z)) implies (( S-max ( L~ z)) .. z) < (( S-min ( L~ z)) .. z)

    proof

      set g = ( Rotate (z,( N-min ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( N-min ( L~ z)) in ( rng z) by SPRECT_2: 39;

      then (g /. 1) = ( N-min ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A2: (( E-max ( L~ g)) .. g) < (( S-max ( L~ g)) .. g) & (( S-max ( L~ g)) .. g) < (( S-min ( L~ g)) .. g) by Lm1, SPRECT_2: 73;

      

       A3: ( S-min ( L~ g)) in ( rng g) by SPRECT_2: 41;

      assume

       A4: (z /. 1) = ( E-max ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A5: ( Rotate (g,( E-max ( L~ z)))) = z by A4, FINSEQ_6: 181;

      ( S-max ( L~ g)) in ( rng g) & ( E-max ( L~ g)) in ( rng g) by SPRECT_2: 42, SPRECT_2: 46;

      hence thesis by A1, A5, A3, A2, Th5;

    end;

    

     Lm20: (z /. 1) = ( S-max ( L~ z)) implies (( N-min ( L~ z)) .. z) < (( E-max ( L~ z)) .. z)

    proof

      assume

       A1: (z /. 1) = ( S-max ( L~ z));

      then (( N-min ( L~ z)) .. z) < (( N-max ( L~ z)) .. z) by Th34;

      hence thesis by A1, Th35, XXREAL_0: 2;

    end;

    

     Lm21: (z /. 1) = ( S-max ( L~ z)) implies (( W-max ( L~ z)) .. z) < (( E-max ( L~ z)) .. z)

    proof

      assume

       A1: (z /. 1) = ( S-max ( L~ z));

      then (( N-min ( L~ z)) .. z) < (( E-max ( L~ z)) .. z) by Lm20;

      hence thesis by A1, Th33, XXREAL_0: 2;

    end;

    

     Lm22: (z /. 1) = ( S-max ( L~ z)) implies (( W-min ( L~ z)) .. z) < (( E-max ( L~ z)) .. z)

    proof

      assume

       A1: (z /. 1) = ( S-max ( L~ z));

      then (( W-min ( L~ z)) .. z) < (( W-max ( L~ z)) .. z) by Th32;

      hence thesis by A1, Lm21, XXREAL_0: 2;

    end;

    

     Lm23: (z /. 1) = ( S-max ( L~ z)) implies (( W-max ( L~ z)) .. z) < (( N-max ( L~ z)) .. z)

    proof

      assume

       A1: (z /. 1) = ( S-max ( L~ z));

      then (( N-min ( L~ z)) .. z) < (( N-max ( L~ z)) .. z) by Th34;

      hence thesis by A1, Th33, XXREAL_0: 2;

    end;

    

     Lm24: (z /. 1) = ( S-max ( L~ z)) implies (( W-min ( L~ z)) .. z) < (( N-min ( L~ z)) .. z)

    proof

      assume

       A1: (z /. 1) = ( S-max ( L~ z));

      then (( W-min ( L~ z)) .. z) < (( W-max ( L~ z)) .. z) by Th32;

      hence thesis by A1, Th33, XXREAL_0: 2;

    end;

    

     Lm25: (z /. 1) = ( S-max ( L~ z)) implies (( S-min ( L~ z)) .. z) < (( N-min ( L~ z)) .. z)

    proof

      assume

       A1: (z /. 1) = ( S-max ( L~ z));

      then (( S-min ( L~ z)) .. z) <= (( W-min ( L~ z)) .. z) by Th31;

      hence thesis by A1, Lm24, XXREAL_0: 2;

    end;

    

     Lm26: (z /. 1) = ( S-max ( L~ z)) implies (( S-min ( L~ z)) .. z) < (( N-max ( L~ z)) .. z)

    proof

      assume

       A1: (z /. 1) = ( S-max ( L~ z));

      then (( S-min ( L~ z)) .. z) < (( N-min ( L~ z)) .. z) by Lm25;

      hence thesis by A1, Th34, XXREAL_0: 2;

    end;

    theorem :: SPRECT_5:41

    

     Th41: (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)

    proof

      set g = ( Rotate (z,( S-max ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( S-max ( L~ z)) in ( rng z) by SPRECT_2: 42;

      then

       A2: (g /. 1) = ( S-max ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A3: (( W-min ( L~ g)) .. g) < (( E-max ( L~ g)) .. g) by Lm22;

      assume that

       A4: (z /. 1) = ( E-max ( L~ z)) and

       A5: ( S-min ( L~ z)) <> ( W-min ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A6: ( Rotate (g,( E-max ( L~ z)))) = z by A4, FINSEQ_6: 181;

      

       A7: ( S-min ( L~ g)) in ( rng g) & ( W-min ( L~ g)) in ( rng g) by SPRECT_2: 41, SPRECT_2: 43;

      ( E-max ( L~ g)) in ( rng g) & (( S-min ( L~ g)) .. g) < (( W-min ( L~ g)) .. g) by A1, A5, A2, Th31, SPRECT_2: 46;

      hence thesis by A1, A6, A7, A3, Th11;

    end;

    theorem :: SPRECT_5:42

    

     Th42: (z /. 1) = ( E-max ( L~ z)) implies (( W-min ( L~ z)) .. z) < (( W-max ( L~ z)) .. z)

    proof

      set g = ( Rotate (z,( S-max ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( S-max ( L~ z)) in ( rng z) by SPRECT_2: 42;

      then (g /. 1) = ( S-max ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A2: (( W-min ( L~ g)) .. g) < (( W-max ( L~ g)) .. g) & (( W-max ( L~ g)) .. g) < (( E-max ( L~ g)) .. g) by Lm21, Th32;

      

       A3: ( E-max ( L~ g)) in ( rng g) by SPRECT_2: 46;

      assume

       A4: (z /. 1) = ( E-max ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A5: ( Rotate (g,( E-max ( L~ z)))) = z by A4, FINSEQ_6: 181;

      ( W-max ( L~ g)) in ( rng g) & ( W-min ( L~ g)) in ( rng g) by SPRECT_2: 43, SPRECT_2: 44;

      hence thesis by A1, A5, A3, A2, Th11;

    end;

    theorem :: SPRECT_5:43

    

     Th43: (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)

    proof

      set g = ( Rotate (z,( S-max ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( S-max ( L~ z)) in ( rng z) by SPRECT_2: 42;

      then

       A2: (g /. 1) = ( S-max ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A3: (( N-min ( L~ g)) .. g) < (( E-max ( L~ g)) .. g) by Lm20;

      assume that

       A4: (z /. 1) = ( E-max ( L~ z)) and

       A5: ( W-max ( L~ z)) <> ( N-min ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A6: ( Rotate (g,( E-max ( L~ z)))) = z by A4, FINSEQ_6: 181;

      

       A7: ( W-max ( L~ g)) in ( rng g) & ( N-min ( L~ g)) in ( rng g) by SPRECT_2: 39, SPRECT_2: 44;

      ( E-max ( L~ g)) in ( rng g) & (( W-max ( L~ g)) .. g) < (( N-min ( L~ g)) .. g) by A1, A5, A2, Th33, SPRECT_2: 46;

      hence thesis by A1, A6, A7, A3, Th11;

    end;

    theorem :: SPRECT_5:44

    (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)

    proof

      set g = ( Rotate (z,( S-max ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      assume

       A2: (z /. 1) = ( E-max ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A3: ( Rotate (g,( E-max ( L~ z)))) = z by A2, FINSEQ_6: 181;

      

       A4: ( N-max ( L~ g)) in ( rng g) & ( N-min ( L~ g)) in ( rng g) by SPRECT_2: 39, SPRECT_2: 40;

      ( S-max ( L~ z)) in ( rng z) by SPRECT_2: 42;

      then

       A5: (g /. 1) = ( S-max ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A6: ( E-max ( L~ g)) in ( rng g) & (( N-min ( L~ g)) .. g) < (( N-max ( L~ g)) .. g) by Th34, SPRECT_2: 46;

      assume ( N-max ( L~ z)) <> ( E-max ( L~ z));

      then (( N-max ( L~ g)) .. g) < (( E-max ( L~ g)) .. g) by A1, A5, Th35;

      hence thesis by A1, A3, A4, A6, Th11;

    end;

    theorem :: SPRECT_5:45

    (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)

    proof

      assume that

       A1: (f /. 1) = ( N-max ( L~ f)) and

       A2: ( N-max ( L~ f)) <> ( E-max ( L~ 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 thesis by A3, A2, A4, FINSEQ_5: 9, XXREAL_0: 1;

    end;

    theorem :: SPRECT_5:46

    (z /. 1) = ( N-max ( L~ z)) implies (( E-max ( L~ z)) .. z) < (( E-min ( L~ z)) .. z)

    proof

      set g = ( Rotate (z,( W-min ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( W-min ( L~ z)) in ( rng z) by SPRECT_2: 43;

      then (g /. 1) = ( W-min ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A2: (( N-max ( L~ g)) .. g) <= (( E-max ( L~ g)) .. g) & (( E-max ( L~ g)) .. g) < (( E-min ( L~ g)) .. g) by Th25, Th26;

      

       A3: ( E-max ( L~ g)) in ( rng g) by SPRECT_2: 46;

      assume

       A4: (z /. 1) = ( N-max ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A5: ( Rotate (g,( N-max ( L~ z)))) = z by A4, FINSEQ_6: 181;

      ( E-min ( L~ g)) in ( rng g) & ( N-max ( L~ g)) in ( rng g) by SPRECT_2: 40, SPRECT_2: 45;

      hence thesis by A1, A5, A3, A2, Th5;

    end;

    theorem :: SPRECT_5:47

    (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)

    proof

      set g = ( Rotate (z,( W-min ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( W-min ( L~ z)) in ( rng z) by SPRECT_2: 43;

      then

       A2: (g /. 1) = ( W-min ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A3: ( S-max ( L~ g)) in ( rng g) & (( N-max ( L~ g)) .. g) < (( E-min ( L~ g)) .. g) by Lm16, SPRECT_2: 42;

      assume that

       A4: (z /. 1) = ( N-max ( L~ z)) and

       A5: ( E-min ( L~ z)) <> ( S-max ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A6: ( Rotate (g,( N-max ( L~ z)))) = z by A4, FINSEQ_6: 181;

      

       A7: ( E-min ( L~ g)) in ( rng g) & ( N-max ( L~ g)) in ( rng g) by SPRECT_2: 40, SPRECT_2: 45;

      (( E-min ( L~ g)) .. g) < (( S-max ( L~ g)) .. g) by A1, A5, A2, Th27;

      hence thesis by A1, A6, A7, A3, Th5;

    end;

    theorem :: SPRECT_5:48

    (z /. 1) = ( N-max ( L~ z)) implies (( S-max ( L~ z)) .. z) < (( S-min ( L~ z)) .. z)

    proof

      set g = ( Rotate (z,( N-min ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( N-min ( L~ z)) in ( rng z) by SPRECT_2: 39;

      then (g /. 1) = ( N-min ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A2: (( S-max ( L~ g)) .. g) < (( S-min ( L~ g)) .. g) & (( N-max ( L~ g)) .. g) < (( S-max ( L~ g)) .. g) by Lm9, SPRECT_2: 73;

      

       A3: ( N-max ( L~ g)) in ( rng g) by SPRECT_2: 40;

      assume

       A4: (z /. 1) = ( N-max ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A5: ( Rotate (g,( N-max ( L~ z)))) = z by A4, FINSEQ_6: 181;

      ( S-max ( L~ g)) in ( rng g) & ( S-min ( L~ g)) in ( rng g) by SPRECT_2: 41, SPRECT_2: 42;

      hence thesis by A1, A5, A3, A2, Th5;

    end;

    theorem :: SPRECT_5:49

    (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)

    proof

      set g = ( Rotate (z,( N-min ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( N-min ( L~ z)) in ( rng z) by SPRECT_2: 39;

      then

       A2: (g /. 1) = ( N-min ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A3: (( N-max ( L~ g)) .. g) < (( S-min ( L~ g)) .. g) by Lm10;

      assume that

       A4: (z /. 1) = ( N-max ( L~ z)) and

       A5: ( S-min ( L~ z)) <> ( W-min ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A6: ( Rotate (g,( N-max ( L~ z)))) = z by A4, FINSEQ_6: 181;

      

       A7: ( W-min ( L~ g)) in ( rng g) & ( S-min ( L~ g)) in ( rng g) by SPRECT_2: 41, SPRECT_2: 43;

      ( N-max ( L~ g)) in ( rng g) & (( S-min ( L~ g)) .. g) < (( W-min ( L~ g)) .. g) by A1, A5, A2, SPRECT_2: 40, SPRECT_2: 74;

      hence thesis by A1, A6, A7, A3, Th5;

    end;

    theorem :: SPRECT_5:50

    (z /. 1) = ( N-max ( L~ z)) implies (( W-min ( L~ z)) .. z) < (( W-max ( L~ z)) .. z)

    proof

      set g = ( Rotate (z,( S-max ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( S-max ( L~ z)) in ( rng z) by SPRECT_2: 42;

      then (g /. 1) = ( S-max ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A2: (( W-min ( L~ g)) .. g) < (( W-max ( L~ g)) .. g) & (( W-max ( L~ g)) .. g) < (( N-max ( L~ g)) .. g) by Lm23, Th32;

      

       A3: ( N-max ( L~ g)) in ( rng g) by SPRECT_2: 40;

      assume

       A4: (z /. 1) = ( N-max ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A5: ( Rotate (g,( N-max ( L~ z)))) = z by A4, FINSEQ_6: 181;

      ( W-min ( L~ g)) in ( rng g) & ( W-max ( L~ g)) in ( rng g) by SPRECT_2: 43, SPRECT_2: 44;

      hence thesis by A1, A5, A3, A2, Th11;

    end;

    theorem :: SPRECT_5:51

    (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)

    proof

      set g = ( Rotate (z,( S-max ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( S-max ( L~ z)) in ( rng z) by SPRECT_2: 42;

      then

       A2: (g /. 1) = ( S-max ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A3: (( N-min ( L~ g)) .. g) < (( N-max ( L~ g)) .. g) by Th34;

      assume that

       A4: (z /. 1) = ( N-max ( L~ z)) and

       A5: ( N-min ( L~ z)) <> ( W-max ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A6: ( Rotate (g,( N-max ( L~ z)))) = z by A4, FINSEQ_6: 181;

      

       A7: ( N-min ( L~ g)) in ( rng g) & ( W-max ( L~ g)) in ( rng g) by SPRECT_2: 39, SPRECT_2: 44;

      ( N-max ( L~ g)) in ( rng g) & (( W-max ( L~ g)) .. g) < (( N-min ( L~ g)) .. g) by A1, A5, A2, Th33, SPRECT_2: 40;

      hence thesis by A1, A6, A7, A3, Th11;

    end;

    theorem :: SPRECT_5:52

    (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)

    proof

      assume that

       A1: (f /. 1) = ( E-min ( L~ f)) and

       A2: ( E-min ( L~ f)) <> ( S-max ( L~ 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 thesis by A3, A2, A4, FINSEQ_5: 9, XXREAL_0: 1;

    end;

    theorem :: SPRECT_5:53

    (z /. 1) = ( E-min ( L~ z)) implies (( S-max ( L~ z)) .. z) < (( S-min ( L~ z)) .. z)

    proof

      set g = ( Rotate (z,( N-min ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( N-min ( L~ z)) in ( rng z) by SPRECT_2: 39;

      then (g /. 1) = ( N-min ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A2: (( E-min ( L~ g)) .. g) <= (( S-max ( L~ g)) .. g) & (( S-max ( L~ g)) .. g) < (( S-min ( L~ g)) .. g) by SPRECT_2: 72, SPRECT_2: 73;

      

       A3: ( S-max ( L~ g)) in ( rng g) by SPRECT_2: 42;

      assume

       A4: (z /. 1) = ( E-min ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A5: ( Rotate (g,( E-min ( L~ z)))) = z by A4, FINSEQ_6: 181;

      ( S-min ( L~ g)) in ( rng g) & ( E-min ( L~ g)) in ( rng g) by SPRECT_2: 41, SPRECT_2: 45;

      hence thesis by A1, A5, A3, A2, Th5;

    end;

    theorem :: SPRECT_5:54

    (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)

    proof

      set g = ( Rotate (z,( N-min ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( N-min ( L~ z)) in ( rng z) by SPRECT_2: 39;

      then

       A2: (g /. 1) = ( N-min ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A3: ( W-min ( L~ g)) in ( rng g) & (( E-min ( L~ g)) .. g) < (( S-min ( L~ g)) .. g) by Lm4, SPRECT_2: 43;

      assume that

       A4: (z /. 1) = ( E-min ( L~ z)) and

       A5: ( S-min ( L~ z)) <> ( W-min ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A6: ( Rotate (g,( E-min ( L~ z)))) = z by A4, FINSEQ_6: 181;

      

       A7: ( S-min ( L~ g)) in ( rng g) & ( E-min ( L~ g)) in ( rng g) by SPRECT_2: 41, SPRECT_2: 45;

      (( S-min ( L~ g)) .. g) < (( W-min ( L~ g)) .. g) by A1, A5, A2, SPRECT_2: 74;

      hence thesis by A1, A6, A7, A3, Th5;

    end;

    

     Lm27: (z /. 1) = ( E-max ( L~ z)) implies (( S-max ( L~ z)) .. z) < (( W-min ( L~ z)) .. z)

    proof

      assume

       A1: (z /. 1) = ( E-max ( L~ z));

      then (( S-max ( L~ z)) .. z) < (( S-min ( L~ z)) .. z) by Th40;

      hence thesis by A1, Th41, XXREAL_0: 2;

    end;

    

     Lm28: (z /. 1) = ( E-max ( L~ z)) implies (( E-min ( L~ z)) .. z) < (( W-min ( L~ z)) .. z)

    proof

      assume

       A1: (z /. 1) = ( E-max ( L~ z));

      then (( E-min ( L~ z)) .. z) <= (( S-max ( L~ z)) .. z) by Th39;

      hence thesis by A1, Lm27, XXREAL_0: 2;

    end;

    

     Lm29: (z /. 1) = ( E-max ( L~ z)) implies (( E-min ( L~ z)) .. z) < (( W-max ( L~ z)) .. z)

    proof

      assume

       A1: (z /. 1) = ( E-max ( L~ z));

      then (( E-min ( L~ z)) .. z) < (( W-min ( L~ z)) .. z) by Lm28;

      hence thesis by A1, Th42, XXREAL_0: 2;

    end;

    

     Lm30: (z /. 1) = ( E-max ( L~ z)) implies (( S-min ( L~ z)) .. z) < (( W-max ( L~ z)) .. z)

    proof

      assume

       A1: (z /. 1) = ( E-max ( L~ z));

      then (( W-min ( L~ z)) .. z) < (( W-max ( L~ z)) .. z) by Th42;

      hence thesis by A1, Th41, XXREAL_0: 2;

    end;

    theorem :: SPRECT_5:55

    (z /. 1) = ( E-min ( L~ z)) implies (( W-min ( L~ z)) .. z) < (( W-max ( L~ z)) .. z)

    proof

      set g = ( Rotate (z,( E-max ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( E-max ( L~ z)) in ( rng z) by SPRECT_2: 46;

      then (g /. 1) = ( E-max ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A2: (( W-min ( L~ g)) .. g) < (( W-max ( L~ g)) .. g) & (( E-min ( L~ g)) .. g) < (( W-min ( L~ g)) .. g) by Lm28, Th42;

      

       A3: ( E-min ( L~ g)) in ( rng g) by SPRECT_2: 45;

      assume

       A4: (z /. 1) = ( E-min ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A5: ( Rotate (g,( E-min ( L~ z)))) = z by A4, FINSEQ_6: 181;

      ( W-min ( L~ g)) in ( rng g) & ( W-max ( L~ g)) in ( rng g) by SPRECT_2: 43, SPRECT_2: 44;

      hence thesis by A1, A5, A3, A2, Th5;

    end;

    theorem :: SPRECT_5:56

    (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)

    proof

      set g = ( Rotate (z,( E-max ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( E-max ( L~ z)) in ( rng z) by SPRECT_2: 46;

      then

       A2: (g /. 1) = ( E-max ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A3: (( E-min ( L~ g)) .. g) < (( W-max ( L~ g)) .. g) by Lm29;

      assume that

       A4: (z /. 1) = ( E-min ( L~ z)) and

       A5: ( W-max ( L~ z)) <> ( N-min ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A6: ( Rotate (g,( E-min ( L~ z)))) = z by A4, FINSEQ_6: 181;

      

       A7: ( N-min ( L~ g)) in ( rng g) & ( W-max ( L~ g)) in ( rng g) by SPRECT_2: 39, SPRECT_2: 44;

      ( E-min ( L~ g)) in ( rng g) & (( W-max ( L~ g)) .. g) < (( N-min ( L~ g)) .. g) by A1, A5, A2, Th43, SPRECT_2: 45;

      hence thesis by A1, A6, A7, A3, Th5;

    end;

    theorem :: SPRECT_5:57

    (z /. 1) = ( E-min ( L~ z)) implies (( N-min ( L~ z)) .. z) < (( N-max ( L~ z)) .. z)

    proof

      set g = ( Rotate (z,( W-min ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( W-min ( L~ z)) in ( rng z) by SPRECT_2: 43;

      then (g /. 1) = ( W-min ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A2: (( N-min ( L~ g)) .. g) < (( N-max ( L~ g)) .. g) & (( N-max ( L~ g)) .. g) < (( E-min ( L~ g)) .. g) by Lm16, Th24;

      

       A3: ( E-min ( L~ g)) in ( rng g) by SPRECT_2: 45;

      assume

       A4: (z /. 1) = ( E-min ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A5: ( Rotate (g,( E-min ( L~ z)))) = z by A4, FINSEQ_6: 181;

      ( N-min ( L~ g)) in ( rng g) & ( N-max ( L~ g)) in ( rng g) by SPRECT_2: 39, SPRECT_2: 40;

      hence thesis by A1, A5, A3, A2, Th11;

    end;

    theorem :: SPRECT_5:58

    (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)

    proof

      set g = ( Rotate (z,( W-min ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( W-min ( L~ z)) in ( rng z) by SPRECT_2: 43;

      then

       A2: (g /. 1) = ( W-min ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A3: (( E-max ( L~ g)) .. g) < (( E-min ( L~ g)) .. g) by Th26;

      assume that

       A4: (z /. 1) = ( E-min ( L~ z)) and

       A5: ( E-max ( L~ z)) <> ( N-max ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A6: ( Rotate (g,( E-min ( L~ z)))) = z by A4, FINSEQ_6: 181;

      

       A7: ( E-max ( L~ g)) in ( rng g) & ( N-max ( L~ g)) in ( rng g) by SPRECT_2: 40, SPRECT_2: 46;

      ( E-min ( L~ g)) in ( rng g) & (( N-max ( L~ g)) .. g) < (( E-max ( L~ g)) .. g) by A1, A5, A2, Th25, SPRECT_2: 45;

      hence thesis by A1, A6, A7, A3, Th11;

    end;

    theorem :: SPRECT_5:59

    (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)

    proof

      assume that

       A1: (f /. 1) = ( S-min ( L~ f)) and

       A2: ( S-min ( L~ f)) <> ( W-min ( L~ 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 thesis by A3, A2, A4, FINSEQ_5: 9, XXREAL_0: 1;

    end;

    theorem :: SPRECT_5:60

    (z /. 1) = ( S-min ( L~ z)) implies (( W-min ( L~ z)) .. z) < (( W-max ( L~ z)) .. z)

    proof

      set g = ( Rotate (z,( E-max ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( E-max ( L~ z)) in ( rng z) by SPRECT_2: 46;

      then (g /. 1) = ( E-max ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A2: (( S-min ( L~ g)) .. g) <= (( W-min ( L~ g)) .. g) & (( W-min ( L~ g)) .. g) < (( W-max ( L~ g)) .. g) by Th41, Th42;

      

       A3: ( W-min ( L~ g)) in ( rng g) by SPRECT_2: 43;

      assume

       A4: (z /. 1) = ( S-min ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A5: ( Rotate (g,( S-min ( L~ z)))) = z by A4, FINSEQ_6: 181;

      ( W-max ( L~ g)) in ( rng g) & ( S-min ( L~ g)) in ( rng g) by SPRECT_2: 41, SPRECT_2: 44;

      hence thesis by A1, A5, A3, A2, Th5;

    end;

    theorem :: SPRECT_5:61

    (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)

    proof

      set g = ( Rotate (z,( E-max ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( E-max ( L~ z)) in ( rng z) by SPRECT_2: 46;

      then

       A2: (g /. 1) = ( E-max ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A3: ( N-min ( L~ g)) in ( rng g) & (( S-min ( L~ g)) .. g) < (( W-max ( L~ g)) .. g) by Lm30, SPRECT_2: 39;

      assume that

       A4: (z /. 1) = ( S-min ( L~ z)) and

       A5: ( W-max ( L~ z)) <> ( N-min ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A6: ( Rotate (g,( S-min ( L~ z)))) = z by A4, FINSEQ_6: 181;

      

       A7: ( W-max ( L~ g)) in ( rng g) & ( S-min ( L~ g)) in ( rng g) by SPRECT_2: 41, SPRECT_2: 44;

      (( W-max ( L~ g)) .. g) < (( N-min ( L~ g)) .. g) by A1, A5, A2, Th43;

      hence thesis by A1, A6, A7, A3, Th5;

    end;

    theorem :: SPRECT_5:62

    (z /. 1) = ( S-min ( L~ z)) implies (( N-min ( L~ z)) .. z) < (( N-max ( L~ z)) .. z)

    proof

      set g = ( Rotate (z,( S-max ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( S-max ( L~ z)) in ( rng z) by SPRECT_2: 42;

      then (g /. 1) = ( S-max ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A2: (( N-min ( L~ g)) .. g) < (( N-max ( L~ g)) .. g) & (( S-min ( L~ g)) .. g) < (( N-min ( L~ g)) .. g) by Lm25, Th34;

      

       A3: ( S-min ( L~ g)) in ( rng g) by SPRECT_2: 41;

      assume

       A4: (z /. 1) = ( S-min ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A5: ( Rotate (g,( S-min ( L~ z)))) = z by A4, FINSEQ_6: 181;

      ( N-min ( L~ g)) in ( rng g) & ( N-max ( L~ g)) in ( rng g) by SPRECT_2: 39, SPRECT_2: 40;

      hence thesis by A1, A5, A3, A2, Th5;

    end;

    theorem :: SPRECT_5:63

    (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)

    proof

      set g = ( Rotate (z,( S-max ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( S-max ( L~ z)) in ( rng z) by SPRECT_2: 42;

      then

       A2: (g /. 1) = ( S-max ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A3: (( S-min ( L~ g)) .. g) < (( N-max ( L~ g)) .. g) by Lm26;

      assume that

       A4: (z /. 1) = ( S-min ( L~ z)) and

       A5: ( N-max ( L~ z)) <> ( E-max ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A6: ( Rotate (g,( S-min ( L~ z)))) = z by A4, FINSEQ_6: 181;

      

       A7: ( E-max ( L~ g)) in ( rng g) & ( N-max ( L~ g)) in ( rng g) by SPRECT_2: 40, SPRECT_2: 46;

      ( S-min ( L~ g)) in ( rng g) & (( N-max ( L~ g)) .. g) < (( E-max ( L~ g)) .. g) by A1, A5, A2, Th35, SPRECT_2: 41;

      hence thesis by A1, A6, A7, A3, Th5;

    end;

    theorem :: SPRECT_5:64

    (z /. 1) = ( S-min ( L~ z)) implies (( E-max ( L~ z)) .. z) < (( E-min ( L~ z)) .. z)

    proof

      set g = ( Rotate (z,( N-min ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( N-min ( L~ z)) in ( rng z) by SPRECT_2: 39;

      then (g /. 1) = ( N-min ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A2: (( E-max ( L~ g)) .. g) < (( E-min ( L~ g)) .. g) & (( E-min ( L~ g)) .. g) < (( S-min ( L~ g)) .. g) by Lm4, SPRECT_2: 71;

      

       A3: ( S-min ( L~ g)) in ( rng g) by SPRECT_2: 41;

      assume

       A4: (z /. 1) = ( S-min ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A5: ( Rotate (g,( S-min ( L~ z)))) = z by A4, FINSEQ_6: 181;

      ( E-max ( L~ g)) in ( rng g) & ( E-min ( L~ g)) in ( rng g) by SPRECT_2: 45, SPRECT_2: 46;

      hence thesis by A1, A5, A3, A2, Th11;

    end;

    theorem :: SPRECT_5:65

    (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)

    proof

      set g = ( Rotate (z,( N-min ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( N-min ( L~ z)) in ( rng z) by SPRECT_2: 39;

      then

       A2: (g /. 1) = ( N-min ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A3: (( S-max ( L~ g)) .. g) < (( S-min ( L~ g)) .. g) by SPRECT_2: 73;

      assume that

       A4: (z /. 1) = ( S-min ( L~ z)) and

       A5: ( S-max ( L~ z)) <> ( E-min ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A6: ( Rotate (g,( S-min ( L~ z)))) = z by A4, FINSEQ_6: 181;

      

       A7: ( S-max ( L~ g)) in ( rng g) & ( E-min ( L~ g)) in ( rng g) by SPRECT_2: 42, SPRECT_2: 45;

      ( S-min ( L~ g)) in ( rng g) & (( E-min ( L~ g)) .. g) < (( S-max ( L~ g)) .. g) by A1, A5, A2, SPRECT_2: 41, SPRECT_2: 72;

      hence thesis by A1, A6, A7, A3, Th11;

    end;

    theorem :: SPRECT_5:66

    (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)

    proof

      assume that

       A1: (f /. 1) = ( W-max ( L~ f)) and

       A2: ( W-max ( L~ f)) <> ( N-min ( L~ 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 thesis by A3, A2, A4, FINSEQ_5: 9, XXREAL_0: 1;

    end;

    theorem :: SPRECT_5:67

    (z /. 1) = ( W-max ( L~ z)) implies (( N-min ( L~ z)) .. z) < (( N-max ( L~ z)) .. z)

    proof

      set g = ( Rotate (z,( S-max ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( S-max ( L~ z)) in ( rng z) by SPRECT_2: 42;

      then (g /. 1) = ( S-max ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A2: (( W-max ( L~ g)) .. g) <= (( N-min ( L~ g)) .. g) & (( N-min ( L~ g)) .. g) < (( N-max ( L~ g)) .. g) by Th33, Th34;

      

       A3: ( N-min ( L~ g)) in ( rng g) by SPRECT_2: 39;

      assume

       A4: (z /. 1) = ( W-max ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A5: ( Rotate (g,( W-max ( L~ z)))) = z by A4, FINSEQ_6: 181;

      ( N-max ( L~ g)) in ( rng g) & ( W-max ( L~ g)) in ( rng g) by SPRECT_2: 40, SPRECT_2: 44;

      hence thesis by A1, A5, A3, A2, Th5;

    end;

    theorem :: SPRECT_5:68

    (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)

    proof

      set g = ( Rotate (z,( S-max ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( S-max ( L~ z)) in ( rng z) by SPRECT_2: 42;

      then

       A2: (g /. 1) = ( S-max ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A3: ( E-max ( L~ g)) in ( rng g) & (( W-max ( L~ g)) .. g) < (( N-max ( L~ g)) .. g) by Lm23, SPRECT_2: 46;

      assume that

       A4: (z /. 1) = ( W-max ( L~ z)) and

       A5: ( N-max ( L~ z)) <> ( E-max ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A6: ( Rotate (g,( W-max ( L~ z)))) = z by A4, FINSEQ_6: 181;

      

       A7: ( N-max ( L~ g)) in ( rng g) & ( W-max ( L~ g)) in ( rng g) by SPRECT_2: 40, SPRECT_2: 44;

      (( N-max ( L~ g)) .. g) < (( E-max ( L~ g)) .. g) by A1, A5, A2, Th35;

      hence thesis by A1, A6, A7, A3, Th5;

    end;

    theorem :: SPRECT_5:69

    (z /. 1) = ( W-max ( L~ z)) implies (( E-max ( L~ z)) .. z) < (( E-min ( L~ z)) .. z)

    proof

      set g = ( Rotate (z,( W-min ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( W-min ( L~ z)) in ( rng z) by SPRECT_2: 43;

      then (g /. 1) = ( W-min ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A2: (( E-max ( L~ g)) .. g) < (( E-min ( L~ g)) .. g) & (( W-max ( L~ g)) .. g) < (( E-max ( L~ g)) .. g) by Lm18, Th26;

      

       A3: ( W-max ( L~ g)) in ( rng g) by SPRECT_2: 44;

      assume

       A4: (z /. 1) = ( W-max ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A5: ( Rotate (g,( W-max ( L~ z)))) = z by A4, FINSEQ_6: 181;

      ( E-max ( L~ g)) in ( rng g) & ( E-min ( L~ g)) in ( rng g) by SPRECT_2: 45, SPRECT_2: 46;

      hence thesis by A1, A5, A3, A2, Th5;

    end;

    theorem :: SPRECT_5:70

    (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)

    proof

      set g = ( Rotate (z,( W-min ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( W-min ( L~ z)) in ( rng z) by SPRECT_2: 43;

      then

       A2: (g /. 1) = ( W-min ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A3: (( W-max ( L~ g)) .. g) < (( E-min ( L~ g)) .. g) by Lm19;

      assume that

       A4: (z /. 1) = ( W-max ( L~ z)) and

       A5: ( E-min ( L~ z)) <> ( S-max ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A6: ( Rotate (g,( W-max ( L~ z)))) = z by A4, FINSEQ_6: 181;

      

       A7: ( S-max ( L~ g)) in ( rng g) & ( E-min ( L~ g)) in ( rng g) by SPRECT_2: 42, SPRECT_2: 45;

      ( W-max ( L~ g)) in ( rng g) & (( E-min ( L~ g)) .. g) < (( S-max ( L~ g)) .. g) by A1, A5, A2, Th27, SPRECT_2: 44;

      hence thesis by A1, A6, A7, A3, Th5;

    end;

    theorem :: SPRECT_5:71

    (z /. 1) = ( W-max ( L~ z)) implies (( S-max ( L~ z)) .. z) < (( S-min ( L~ z)) .. z)

    proof

      set g = ( Rotate (z,( E-max ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( E-max ( L~ z)) in ( rng z) by SPRECT_2: 46;

      then (g /. 1) = ( E-max ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A2: (( S-max ( L~ g)) .. g) < (( S-min ( L~ g)) .. g) & (( S-min ( L~ g)) .. g) < (( W-max ( L~ g)) .. g) by Lm30, Th40;

      

       A3: ( W-max ( L~ g)) in ( rng g) by SPRECT_2: 44;

      assume

       A4: (z /. 1) = ( W-max ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A5: ( Rotate (g,( W-max ( L~ z)))) = z by A4, FINSEQ_6: 181;

      ( S-max ( L~ g)) in ( rng g) & ( S-min ( L~ g)) in ( rng g) by SPRECT_2: 41, SPRECT_2: 42;

      hence thesis by A1, A5, A3, A2, Th11;

    end;

    theorem :: SPRECT_5:72

    (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)

    proof

      set g = ( Rotate (z,( E-max ( L~ z))));

      

       A1: ( L~ z) = ( L~ g) by REVROT_1: 33;

      ( E-max ( L~ z)) in ( rng z) by SPRECT_2: 46;

      then

       A2: (g /. 1) = ( E-max ( L~ g)) by A1, FINSEQ_6: 92;

      then

       A3: (( W-min ( L~ g)) .. g) < (( W-max ( L~ g)) .. g) by Th42;

      assume that

       A4: (z /. 1) = ( W-max ( L~ z)) and

       A5: ( W-min ( L~ z)) <> ( S-min ( L~ z));

      for i be Nat st 1 < i & i < ( len z) holds (z /. i) <> (z /. 1) by GOBOARD7: 36;

      then

       A6: ( Rotate (g,( W-max ( L~ z)))) = z by A4, FINSEQ_6: 181;

      

       A7: ( W-min ( L~ g)) in ( rng g) & ( S-min ( L~ g)) in ( rng g) by SPRECT_2: 41, SPRECT_2: 43;

      ( W-max ( L~ g)) in ( rng g) & (( S-min ( L~ g)) .. g) < (( W-min ( L~ g)) .. g) by A1, A5, A2, Th41, SPRECT_2: 44;

      hence thesis by A1, A6, A7, A3, Th11;

    end;