theorem :: NAT_6:27

for a being integer number holds Leg (a,2) = a mod 2