A1: for x being Real st x in ].(- (PI / 2)),(PI / 2).[ holds
diff (sin,x) > 0

proof

let x be Real; :: thesis: ( x in ].(- (PI / 2)),(PI / 2).[ implies diff (sin,x) > 0 )
assume x in ].(- (PI / 2)),(PI / 2).[ ; :: thesis: diff (sin,x) > 0
then 0 < cos . x by Th11;
hence diff (sin,x) > 0 by SIN_COS:68; :: thesis: verum

end;

].(- (PI / 2)),(PI / 2).[ is open by RCOMP_1:7;
hence sin | ].(- (PI / 2)),(PI / 2).[ is increasing by A1, FDIFF_1:26, ROLLE:9, SIN_COS:24, SIN_COS:68; :: thesis: verum