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