set f = sin | [.(- (PI / 2)),(PI / 2).];
( (sin | [.(- (PI / 2)),(PI / 2).]) .: [.(- (PI / 2)),(PI / 2).] = [.(- 1),1.] & (((sin | [.(- (PI / 2)),(PI / 2).]) | [.(- (PI / 2)),(PI / 2).]) ") | ((sin | [.(- (PI / 2)),(PI / 2).]) .: [.(- (PI / 2)),(PI / 2).]) is increasing ) by Th45, COMPTRIG:23, FCONT_3:9, RELAT_1:129;
hence arcsin | [.(- 1),1.] is increasing by RELAT_1:72; :: thesis: verum