let a be Integer; :: thesis: Leg (a,2) = a mod 2

per cases ( a is even or a is odd ) ;

suppose A1: a is even ; :: thesis: Leg (a,2) = a mod 2

then a mod 2 = 0 by INT_1:62;
hence Leg (a,2) = a mod 2 by A1, Def3; :: thesis: verum

end;

suppose A2: a is odd ; :: thesis: Leg (a,2) = a mod 2

reconsider amod2 = a mod 2 as Element of NAT by INT_1:3, INT_1:57;
A3: ( amod2 = 0 or amod2 = 1 ) by NAT_1:23, INT_1:58;
a - 1 = (((a div 2) * 2) + 1) - 1 by A3, A2, INT_1:62, INT_1:59;
then A4: 1,a are_congruent_mod 2 by INT_1:def 5, INT_1:14;
a gcd 2 <= 2 by INT_2:27, INT_2:21;
then A5: not not a gcd 2 = 0 & ... & not a gcd 2 = 2 ;
1 |^ (1 + 1) = 1 ;
hence Leg (a,2) = a mod 2 by A4, INT_2:5, A5, INT_2:21, A3, A2, INT_1:62, Def3, Th22; :: thesis: verum

end;

end;