let f be V19() standard special_circular_sequence; 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); ( 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 )
; 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; verum