let n be Nat; :: thesis: ( 0 < 1 / (n + 1) & 1 / (n + 1) < PI - (1 / (n + 1)) & PI - (1 / (n + 1)) < PI & [.(1 / (n + 1)),(PI - (1 / (n + 1))).] c= ].0,PI.[ & ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] = [.(1 / (n + 1)),(PI - (1 / (n + 1))).] )
thus 0 < 1 / (n + 1) ; :: thesis: ( 1 / (n + 1) < PI - (1 / (n + 1)) & PI - (1 / (n + 1)) < PI & [.(1 / (n + 1)),(PI - (1 / (n + 1))).] c= ].0,PI.[ & ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] = [.(1 / (n + 1)),(PI - (1 / (n + 1))).] )
0 + 1 <= n + 1 by XREAL_1:7;
then 1 / (n + 1) <= (n + 1) / (n + 1) by XREAL_1:72;
then A1: 1 / (n + 1) <= 1 by XCMPLX_1:60;
A2: (313 / 100) - (1 / (n + 1)) < PI - (1 / (n + 1)) by LEIBNIZ1:17, XREAL_1:14;
A3: (313 / 100) - 1 <= (313 / 100) - (1 / (n + 1)) by A1, XREAL_1:13;
1 / (n + 1) < (313 / 100) - 1 by XXREAL_0:2, A1;
then A4: 1 / (n + 1) < (313 / 100) - (1 / (n + 1)) by A3, XXREAL_0:2;
hence 1 / (n + 1) < PI - (1 / (n + 1)) by A2, XXREAL_0:2; :: thesis: ( PI - (1 / (n + 1)) < PI & [.(1 / (n + 1)),(PI - (1 / (n + 1))).] c= ].0,PI.[ & ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] = [.(1 / (n + 1)),(PI - (1 / (n + 1))).] )
PI - (1 / (n + 1)) < PI - 0 by XREAL_1:15;
hence PI - (1 / (n + 1)) < PI ; :: thesis: ( [.(1 / (n + 1)),(PI - (1 / (n + 1))).] c= ].0,PI.[ & ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] = [.(1 / (n + 1)),(PI - (1 / (n + 1))).] )
hence [.(1 / (n + 1)),(PI - (1 / (n + 1))).] c= ].0,PI.[ by XXREAL_1:47; :: thesis: ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] = [.(1 / (n + 1)),(PI - (1 / (n + 1))).]
thus ['(1 / (n + 1)),(PI - (1 / (n + 1)))'] = [.(1 / (n + 1)),(PI - (1 / (n + 1))).] by A2, A4, INTEGRA5:def 3, XXREAL_0:2; :: thesis: verum