let i be Integer; :: thesis: ( i mod 2 = 0 or i mod 2 = 1 )
set A = (i div 2) * 2;
set M = i mod 2;
i div 2 = [\(i / 2)/] by INT_1:def 7;
then ( (i / 2) - 1 < i div 2 & i div 2 <= i / 2 ) by INT_1:def 4;
then ( ((i / 2) - 1) * 2 < (i div 2) * 2 & (i div 2) * 2 <= (i / 2) * 2 ) by XREAL_1:66, XREAL_1:70;
then ( - (i - 2) > - ((i div 2) * 2) & - i <= - ((i div 2) * 2) ) by XREAL_1:26;
then ( i + (2 - i) > i + (- ((i div 2) * 2)) & i + (- i) <= i + (- ((i div 2) * 2)) ) by XREAL_1:8;
then ( 2 > i - ((i div 2) * 2) & 0 <= i - ((i div 2) * 2) ) ;
then A1: ( 2 > i mod 2 & 0 <= i mod 2 ) by INT_1:def 8;
then reconsider M = i mod 2 as Element of NAT by INT_1:16;
M in { k where k is Element of NAT : k < 2 } by A1;
then M in 2 by AXIOMS:30;
hence ( i mod 2 = 0 or i mod 2 = 1 ) by CARD_1:88, TARSKI:def 2; :: thesis: verum