[.(- (PI / 4)),(PI / 4).] c= ].(- (PI / 2)),(PI / 2).[ by Lm7, Lm8, XXREAL_2:def 12;
then tan | [.(- (PI / 4)),(PI / 4).] is increasing by Th7, RFUNCT_2:28;
hence (tan | [.(- (PI / 4)),(PI / 4).]) | [.(- (PI / 4)),(PI / 4).] is increasing ; :: thesis: verum