theorem Th53: :: SIN_COS6:53
for i being Integer holds sin | [.((- (PI / 2)) + ((2 * PI) * i)),((PI / 2) + ((2 * PI) * i)).] is increasing