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