let p be Point of (TOP-REAL 2); :: thesis: for f being non constant standard special_circular_sequence st Rotate (f,p) is clockwise_oriented holds
f is clockwise_oriented
let f be non constant standard special_circular_sequence; :: thesis: ( Rotate (f,p) is clockwise_oriented implies f is clockwise_oriented )
assume Rotate (f,p) is clockwise_oriented ; :: thesis: f is clockwise_oriented
then reconsider g = Rotate (f,p) as non constant standard clockwise_oriented special_circular_sequence ;
for i being Nat st 1 < i & i < len f holds
f /. i <> f /. 1 by GOBOARD7:36;
then f = Rotate (g,(f /. 1)) by FINSEQ_6:181;
hence f is clockwise_oriented ; :: thesis: verum