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 and
A5: p2 .. f < p3 .. f ; :: thesis: p1 .. (Rotate f,p3) < p2 .. (Rotate f,p3)
p1 .. f < p3 .. f by A4, A5, XXREAL_0:2;
then A6: p1 .. (Rotate f,p3) = ((len f) + (p1 .. f)) - (p3 .. f) by A1, A3, Th10;
A7: p2 .. (Rotate f,p3) = ((len f) + (p2 .. f)) - (p3 .. f) by A2, A3, A5, Th10;
(len f) + (p1 .. f) < (len f) + (p2 .. f) by A4, XREAL_1:8;
hence p1 .. (Rotate f,p3) < p2 .. (Rotate f,p3) by A6, A7, XREAL_1:11; :: thesis: verum