theorem Th20: :: BASEL_1:22

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