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; verum