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

proof

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

end;

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