let D be non empty set ; :: thesis:
let f be FinSequence of D; :: thesis:
let p1, p2, p3 be Element of D; :: thesis:
assume that
A1: p1 in rng f and
A2: ( p2 in rng f & p3 in rng f ) and
A3: p1 .. f < p2 .. f and
A4: p2 .. f <= p3 .. f ; :: thesis:

hence p2 .. (Rotate (f,p1)) <= p3 .. (Rotate (f,p1)) by A1, A2, A3, Th5; :: thesis:

end;

end;