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 .. (Rotate f,p2) = ((len f) + (p1 .. f)) - (p2 .. f) by A1, A2, A4, Th10;
A7: p3 .. (Rotate f,p2) = ((p3 .. f) - (p2 .. f)) + 1 by A2, A3, A5, Th4
.= ((p3 .. f) + 1) - (p2 .. f) ;
A8: 1 <= p1 .. f by A1, FINSEQ_4:31;
p3 .. f <= len f by A3, FINSEQ_4:31;
then (p3 .. f) + 1 <= (len f) + (p1 .. f) by A8, XREAL_1:9;
then A9: p3 .. (Rotate f,p2) <= p1 .. (Rotate f,p2) by A6, A7, XREAL_1:11;
A10: p1 in rng (Rotate f,p2) by A1, A2, FINSEQ_6:96;
p3 in rng (Rotate f,p2) by A2, A3, FINSEQ_6:96;
hence p3 .. (Rotate f,p2) < p1 .. (Rotate f,p2) by A4, A5, A9, A10, FINSEQ_5:10, XXREAL_0:1; :: thesis: verum