let i be Integer; :: thesis: ( 3 * i <= 1 & 0 < 1 + (3 * i) implies i = 0 )
assume that
A1: 3 * i <= 1 and
A2: 0 < 1 + (3 * i) ; :: thesis: i = 0
assume A3: not i = 0 ; :: thesis: contradiction

per cases then ( i < 0 or i > 0 ) ;

suppose i < 0 ; :: thesis: contradiction

then consider k being Nat such that
A4: i = - k by Lm3;
0 + (3 * k) < (1 - (3 * k)) + (3 * k) by A2, A4, XREAL_1:8;
then A5: (3 * k) / 3 < 1 / 3 by XREAL_1:74;
k <> 0 by A3, A4;
then consider j being Nat such that
A6: k = j + 1 by NAT_1:6;
(j + 1) - 1 < (1 / 3) - 1 by A6, A5, XREAL_1:8;
then j + 0 < - (2 / 3) ;
hence contradiction by NAT_1:2; :: thesis: verum

end;

suppose A7: i > 0 ; :: thesis: contradiction

then consider k being Nat such that
A8: i = k by Lm2;
consider j being Nat such that
A9: k = j + 1 by A7, A8, NAT_1:6;
(k * 3) / 3 <= 1 / 3 by A1, A8, XREAL_1:72;
then (j + 1) - 1 <= (1 / 3) - 1 by A9, XREAL_1:9;
then j + 0 <= - (2 / 3) ;
hence contradiction by NAT_1:2; :: thesis: verum

end;

end;