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 Element of NAT st 1 < i & i < len f holds
f /. i <> f /. 1 by GOBOARD7:38;
then f = Rotate g,(f /. 1) by REVROT_1:16;
hence f is clockwise_oriented ; :: thesis: verum