[.((3 / 4) * PI),PI.] c= ].(PI / 2),PI.] by Lm6, XXREAL_2:def 12;
then (sec | ].(PI / 2),PI.]) | [.((3 / 4) * PI),PI.] = sec | [.((3 / 4) * PI),PI.] by RELAT_1:74;
hence sec | [.((3 / 4) * PI),PI.] is one-to-one ; :: thesis: verum