rng (x_r-seq m) c= ].0,(PI / 2).[ by Th20;
hence rng (x_r-seq m) c= REAL by XBOOLE_1:1; :: according to RELAT_1:def 19 :: thesis: verum