theorem Th21: :: BASEL_1:23

for k, m being Nat st 1 <= k & k <= m holds
( 0 < (x_r-seq m) . k & (x_r-seq m) . k < PI / 2 )