for m being Nat holds rng (x_r-seq m) c= ].0,(PI / 2).[