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:148
.= rng (tan | ].(- (PI / 2)),(PI / 2).[) by RELAT_1:102
.= tan .: ].(- (PI / 2)),(PI / 2).[ by RELAT_1:148 ;
(tan | ].(- (PI / 2)),(PI / 2).[) | ].(- (PI / 2)),(PI / 2).[ = tan | ].(- (PI / 2)),(PI / 2).[ by RELAT_1:102;
hence arctan | (tan .: ].(- (PI / 2)),(PI / 2).[) is increasing by A1, Th7, FCONT_3:17; :: thesis: verum