let f be 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