set f = tan | ].(- (PI / 2)),(PI / 2).[;
A1: (tan | ].(- (PI / 2)),(PI / 2).[) .: ].(- (PI / 2)),(PI / 2).[ = rng ((tan | ].(- (PI / 2)),(PI / 2).[) | ].(- (PI / 2)),(PI / 2).[) by RELAT_1:115
.= rng (tan | ].(- (PI / 2)),(PI / 2).[) by RELAT_1:73
.= tan .: ].(- (PI / 2)),(PI / 2).[ by RELAT_1:115 ;
(tan | ].(- (PI / 2)),(PI / 2).[) | ].(- (PI / 2)),(PI / 2).[ = tan | ].(- (PI / 2)),(PI / 2).[ by RELAT_1:73;
hence arctan | (tan .: ].(- (PI / 2)),(PI / 2).[) is increasing by A1, Th7, FCONT_3:9; :: thesis: verum