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
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, 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 p1 .. (Rotate (f,p3)) < p2 .. (Rotate (f,p3)) by A5, XREAL_1:9; :: thesis: verum