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 & p2 in rng f ) and
A2: p3 in rng f and
A3: p1 .. f <= p2 .. f and
A4: p2 .. f < p3 .. f ; :: thesis: p1 .. (Rotate (f,p3)) <= p2 .. (Rotate (f,p3))

per cases ( p1 .. f < p2 .. f or p1 .. f = p2 .. f ) by A3, XXREAL_0:1;

suppose p1 .. f < p2 .. f ; :: thesis: p1 .. (Rotate (f,p3)) <= p2 .. (Rotate (f,p3))

hence p1 .. (Rotate (f,p3)) <= p2 .. (Rotate (f,p3)) by A1, A2, A4, Th11; :: thesis: verum

end;

suppose p1 .. f = p2 .. f ; :: thesis: p1 .. (Rotate (f,p3)) <= p2 .. (Rotate (f,p3))

hence p1 .. (Rotate (f,p3)) <= p2 .. (Rotate (f,p3)) by A1, FINSEQ_5:9; :: thesis: verum

end;

end;