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