for t being Real holds ((t ^2) - 1) / ((t ^2) + 1) < 1