A1: [.((3 / 4) * PI),PI.] c= ].(PI / 2),PI.] by Lm6, XXREAL_2:def 12;
rng (sec | [.((3 / 4) * PI),PI.]) c= rng (sec | ].(PI / 2),PI.])
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (sec | [.((3 / 4) * PI),PI.]) or y in rng (sec | ].(PI / 2),PI.]) )
assume y in rng (sec | [.((3 / 4) * PI),PI.]) ; :: thesis: y in rng (sec | ].(PI / 2),PI.])
then y in sec .: [.((3 / 4) * PI),PI.] by RELAT_1:115;
then ex x being object st
( x in dom sec & x in [.((3 / 4) * PI),PI.] & y = sec . x ) by FUNCT_1:def 6;
then y in sec .: ].(PI / 2),PI.] by A1, FUNCT_1:def 6;
hence y in rng (sec | ].(PI / 2),PI.]) by RELAT_1:115; :: thesis: verum
end;
hence [.(- (sqrt 2)),(- 1).] c= dom arcsec2 by Th42, FUNCT_1:33; :: thesis: verum